use good old MePo filter for SMT solvers by default, since arithmetic is built-in for them

--- 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