1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -688,7 +688,8 @@
     1.4          case fact_filter of
     1.5            SOME ff => (() |> ff <> mepoN ? maybe_learn; ff)
     1.6          | NONE =>
     1.7 -          if mash_can_suggest_facts ctxt then (maybe_learn (); meshN)
     1.8 +          if is_smt_prover ctxt prover then mepoN
     1.9 +          else if mash_can_suggest_facts ctxt then (maybe_learn (); meshN)
    1.10            else if mash_could_suggest_facts () then (maybe_learn (); mepoN)
    1.11            else mepoN
    1.12        val add_ths = Attrib.eval_thms ctxt add