tuned proof preplay to explicitly refer to Z3 backend

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Nov 30 22:00:23 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Dec 01 15:29:54 2020 +0100
@@ -160,7 +160,7 @@
 
             fun massage_methods (meths as meth :: _) =
               if not try0 then [meth]
-              else if smt_proofs then SMT_Method SMT_Default :: meths
+              else if smt_proofs then SMT_Method SMT_Z3 :: meths
               else meths
 
             val (params, _, concl_t) = strip_subgoal goal subgoal ctxt

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Mon Nov 30 22:00:23 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Dec 01 15:29:54 2020 +0100
@@ -10,7 +10,7 @@
   type stature = ATP_Problem_Generate.stature
 
   datatype SMT_backend =
-    SMT_Default |
+    SMT_Z3 |
     SMT_Verit of string
 
   datatype proof_method =
@@ -53,7 +53,7 @@
 open ATP_Proof_Reconstruct
 
 datatype SMT_backend =
-  SMT_Default |
+  SMT_Z3 |
   SMT_Verit of string
 
 datatype proof_method =
@@ -101,7 +101,7 @@
       | Metis_Method (type_enc_opt, lam_trans_opt) =>
         "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
       | Meson_Method => "meson"
-      | SMT_Method SMT_Default => "smt"
+      | SMT_Method SMT_Z3 => "smt (z3)"
       | SMT_Method (SMT_Verit strategy) =>
         "smt (" ^ commas ("verit" :: (if strategy = "default" then [] else [strategy])) ^ ")"
       | SATx_Method => "satx"
@@ -130,7 +130,7 @@
           global_facts) ctxt local_facts)
       end
 
-    fun tac_of_smt SMT_Default = SMT_Solver.smt_tac
+    fun tac_of_smt SMT_Z3 = SMT_Solver.smt_tac
       | tac_of_smt (SMT_Verit strategy) = Verit_Proof.verit_tac_stgy strategy
   in
     (case meth of

--- 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

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Nov 30 22:00:23 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Tue Dec 01 15:29:54 2020 +0100
@@ -202,7 +202,7 @@
           val _ = found_proof ();
           val preferred =
             if smt_proofs then
-              SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Default)
+              SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Z3)
             else
               Metis_Method (NONE, NONE);
           val methss = bunches_of_proof_methods ctxt try0 smt_proofs false liftingN;