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.ML
changeset 74370 d8dc8fdc46fc
parent 73940 f58108b7a60c
child 74897 8b1ab558e3ee 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Tue Sep 28 10:38:36 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Tue Sep 28 10:47:18 2021 +0200
@@ -189,9 +189,8 @@
 
     val smt_methodss =
       if smt_proofs then
-        [SMT_Method SMT_Z3 ::
-         map (fn strategy => SMT_Method (SMT_Verit strategy))
-           (Verit_Proof.all_veriT_stgies (Context.Proof ctxt))]
+        [map (SMT_Method o SMT_Verit) (Verit_Proof.all_veriT_stgies (Context.Proof ctxt)),
+         [SMT_Method SMT_Z3]]
       else
         []
   in
isabelle