Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
changeset 75868 e7b04452eef3
parent 75371 136f79711c2a
child 77269 bc43f86c9598 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Tue Aug 16 10:39:44 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Tue Aug 16 17:24:58 2022 +0200
@@ -145,7 +145,11 @@
               SMT_Method (if name = "z3" then SMT_Z3 else SMT_Verit "default")
             else
               Metis_Method (NONE, NONE);
-          val methss = bunches_of_proof_methods ctxt try0 smt_proofs false liftingN;
+          val methss =
+            if try0 then
+              bunches_of_proof_methods ctxt smt_proofs false liftingN
+            else
+              [[preferred]]
         in
           ((preferred, methss),
            fn preplay =>
isabelle