# HG changeset patch
# User blanchet
# Date 1406757176 -7200
# Node ID 892e8e7a42b31f70ea00444a65ed9d4cb42125db
# Parent  949838aba4874c6801de52f3bbb68db9880243cb
added more proof methods for one-liners

diff -r 949838aba487 -r 892e8e7a42b3 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Jul 30 23:52:56 2014 +0200
@@ -182,14 +182,15 @@
   | _ => "Try this")
 
 fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
+  [Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE),
+   Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Meson_Method, Blast_Method,
+   Linarith_Method, Presburger_Method] @
   (if needs_full_types then
-     [Metis_Method (SOME full_typesN, NONE),
-      Metis_Method (SOME really_full_type_enc, NONE),
+     [Metis_Method (SOME really_full_type_enc, NONE),
       Metis_Method (SOME full_typesN, SOME desperate_lam_trans),
       Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]
    else
-     [Metis_Method (NONE, NONE),
-      Metis_Method (SOME full_typesN, NONE),
+     [Metis_Method (SOME full_typesN, NONE),
       Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
       Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]) @
   (if smt_proofs then [SMT2_Method] else [])
@@ -234,18 +235,11 @@
       let
         val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
         val ths = pairs |> sort_wrt (fst o fst) |> map snd
+
         fun play [] [] = (get_preferred meths, Play_Failed)
           | play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout)
           | play timed_out (meth :: meths) =
-            let
-              val _ =
-                if verbose then
-                  Output.urgent_message ("Trying \"" ^ string_of_proof_method ctxt [] meth ^
-                    "\" for " ^ string_of_time timeout ^ "...")
-                else
-                  ()
-              val timer = Timer.startRealTimer ()
-            in
+            let val timer = Timer.startRealTimer () in
               (case timed_proof_method timeout ths meth state i of
                 SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
               | _ => play timed_out meths)