# HG changeset patch
# User blanchet
# Date 1412081654 -7200
# Node ID 59bdd4f5725583f2dfd35869d1d663b3f530d71d
# Parent  20aaa307c0ff07336d757e82f45ea886bbffe6ac
tuned output in case of one-liner failure

diff -r 20aaa307c0ff -r 59bdd4f57255 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Tue Sep 30 14:40:48 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Tue Sep 30 14:54:14 2014 +0200
@@ -159,7 +159,7 @@
   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   | _ => "Try this")
 
-fun bunches_of_proof_methods try0 smt_proofs needs_full_types desperate_lam_trans =
+fun bunches_of_proof_methods try0 smt_method needs_full_types desperate_lam_trans =
   (if try0 then
     [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method],
      [Meson_Method, Fastforce_Method, Force_Method, Presburger_Method]]
@@ -175,7 +175,7 @@
       [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 [[SMT_Method]] else [])
+  (if smt_method then [[SMT_Method]] else [])
 
 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
 
diff -r 20aaa307c0ff -r 59bdd4f57255 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Tue Sep 30 14:40:48 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Tue Sep 30 14:54:14 2014 +0200
@@ -196,8 +196,10 @@
       (case outcome of
         NONE =>
         let
+          val smt_method = smt_proofs <> SOME false
           val preferred_methss =
-            (SMT_Method, bunches_of_proof_methods try0 (smt_proofs <> SOME false) false liftingN)
+            (if smt_method then SMT_Method else Metis_Method (NONE, NONE),
+             bunches_of_proof_methods try0 smt_method false liftingN)
         in
           (preferred_methss,
            fn preplay =>