# 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