# HG changeset patch
# User blanchet
# Date 1406897037 -7200
# Node ID 1977a884fef72d8b834c6ef05b0d7c9c4ff1839c
# Parent  a35d2d26d66e995a7d00c0dca43b658f502a0b96
honor 'try0' also for one-liners

diff -r a35d2d26d66e -r 1977a884fef7 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -67,7 +67,7 @@
   val overlord_file_location_of_prover : string -> string * string
   val proof_banner : mode -> string -> string
   val is_atp : theory -> string -> bool
-  val bunches_of_proof_methods : bool -> bool -> string -> proof_method list list
+  val bunches_of_proof_methods : bool -> bool -> bool -> string -> proof_method list list
   val is_fact_chained : (('a * stature) * 'b) -> bool
   val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
     ((''a * stature) * 'b) list
@@ -161,19 +161,22 @@
   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   | _ => "Try this")
 
-fun bunches_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
-  [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method],
-   [Meson_Method, Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE),
-    Force_Method, Presburger_Method],
-    (if needs_full_types then
-       [Metis_Method (NONE, 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 (SOME full_typesN, NONE),
-        Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
-        Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)])] @
+fun bunches_of_proof_methods try0 smt_proofs needs_full_types desperate_lam_trans =
+  (if try0 then
+    [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method],
+     [Meson_Method, Force_Method, Presburger_Method]]
+   else
+     []) @
+  [[Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE)],
+   (if needs_full_types then
+      [Metis_Method (NONE, 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 (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 [])
 
 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
diff -r a35d2d26d66e -r 1977a884fef7 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -360,7 +360,7 @@
           val used_facts = used_facts_in_atp_proof ctxt (map fst used_from) atp_proof
           val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
           val preferred_methss =
-            bunches_of_proof_methods (smt_proofs <> SOME false) needs_full_types
+            bunches_of_proof_methods try0 (smt_proofs <> SOME false) needs_full_types
               (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)
             |> `(hd o hd)
         in
diff -r a35d2d26d66e -r 1977a884fef7 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -197,7 +197,7 @@
         NONE =>
         let
           val preferred_methss =
-            (SMT2_Method, bunches_of_proof_methods (smt_proofs <> SOME false) false liftingN)
+            (SMT2_Method, bunches_of_proof_methods try0 (smt_proofs <> SOME false) false liftingN)
         in
           (preferred_methss,
            fn preplay =>