# HG changeset patch # User blanchet # Date 1342815586 -7200 # Node ID b903ea11b3bca0bd0871ef9ae2e609b86f2cd1e4 # Parent 2779dea0b1e0477e65c2f87cf7f64a73f26e7857 use good old MePo filter for SMT solvers by default, since arithmetic is built-in for them diff -r 2779dea0b1e0 -r b903ea11b3bc src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200 @@ -688,7 +688,8 @@ case fact_filter of SOME ff => (() |> ff <> mepoN ? maybe_learn; ff) | NONE => - if mash_can_suggest_facts ctxt then (maybe_learn (); meshN) + if is_smt_prover ctxt prover then mepoN + else if mash_can_suggest_facts ctxt then (maybe_learn (); meshN) else if mash_could_suggest_facts () then (maybe_learn (); mepoN) else mepoN val add_ths = Attrib.eval_thms ctxt add