src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML

   type stature = ATP_Problem_Generate.stature
 
   datatype proof_method =
     Metis_Method of string option * string option |
     Meson_Method |
-    SMT2_Method |
+    SMT_Method |
     SATx_Method |
     Blast_Method |
     Simp_Method |
     Simp_Size_Method |
     Auto_Method |

 open ATP_Proof_Reconstruct
 
 datatype proof_method =
   Metis_Method of string option * string option |
   Meson_Method |
-  SMT2_Method |
+  SMT_Method |
   SATx_Method |
   Blast_Method |
   Simp_Method |
   Simp_Size_Method |
   Auto_Method |

 type one_line_params =
   ((string * stature) list * (proof_method * play_outcome)) * string * int * int
 
 fun is_proof_method_direct (Metis_Method _) = true
   | is_proof_method_direct Meson_Method = true
-  | is_proof_method_direct SMT2_Method = true
+  | is_proof_method_direct SMT_Method = true
   | is_proof_method_direct Simp_Method = true
   | is_proof_method_direct Simp_Size_Method = true
   | is_proof_method_direct _ = false
 
 fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")"

       (case meth of
         Metis_Method (NONE, NONE) => "metis"
       | Metis_Method (type_enc_opt, lam_trans_opt) =>
         "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
       | Meson_Method => "meson"
-      | SMT2_Method => "smt2"
+      | SMT_Method => "smt"
       | SATx_Method => "satx"
       | Blast_Method => "blast"
       | Simp_Method => if null ss then "simp" else "simp add:"
       | Simp_Size_Method => "simp add: " ^ short_thm_name ctxt @{thm size_ne_size_imp_ne}
       | Auto_Method => "auto"

     let val ctxt = Config.put Metis_Tactic.verbose false ctxt in
       Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
         (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
     end
   | Meson_Method => Meson_Tactic.meson_general_tac (silence_methods ctxt) global_facts
-  | SMT2_Method =>
-    let val ctxt = Config.put SMT2_Config.verbose false ctxt in
-      SMT2_Solver.smt2_tac ctxt global_facts
+  | SMT_Method =>
+    let val ctxt = Config.put SMT_Config.verbose false ctxt in
+      SMT_Solver.smt_tac ctxt global_facts
     end
   | Simp_Method => Simplifier.asm_full_simp_tac (silence_methods ctxt addsimps global_facts)
   | Simp_Size_Method =>
     Simplifier.asm_full_simp_tac
       (silence_methods ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts))