use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Oct 15 15:26:58 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Oct 15 15:31:18 2013 +0200
@@ -281,7 +281,9 @@
     val lam_trans = lookup_option lookup_string "lam_trans"
     val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
     val learn = lookup_bool "learn"
-    val fact_filter = lookup_option lookup_string "fact_filter"
+    val fact_filter =
+      lookup_option lookup_string "fact_filter"
+      |> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf)
     val max_facts = lookup_option lookup_int "max_facts"
     val fact_thresholds = lookup_real_pair "fact_thresholds"
     val max_mono_iters = lookup_option lookup_int "max_mono_iters"
@@ -291,12 +293,10 @@
     val isar_compress = Real.max (1.0, lookup_real "isar_compress")
     val isar_try0 = lookup_bool "isar_try0"
     val slice = mode <> Auto_Try andalso lookup_bool "slice"
-    val minimize =
-      if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
+    val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
     val timeout = if mode = Auto_Try then NONE else lookup_time "timeout"
     val preplay_timeout =
-      if mode = Auto_Try then SOME Time.zeroTime
-      else lookup_time "preplay_timeout"
+      if mode = Auto_Try then SOME Time.zeroTime else lookup_time "preplay_timeout"
     val expect = lookup_string "expect"
   in
     {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking,