src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Nov 30 22:00:23 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Tue Dec 01 15:29:54 2020 +0100
@@ -177,7 +177,7 @@
 
     val smt_methodss =
       if smt_proofs then
-        [SMT_Method SMT_Default ::
+        [SMT_Method SMT_Z3 ::
          map (fn strategy => SMT_Method (SMT_Verit strategy))
            (Verit_Proof.all_veriT_stgies (Context.Proof ctxt))]
       else