src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

 val vampire_skolemisation_rule = "skolemisation"
 val veriT_la_generic_rule = "la_generic"
 val veriT_simp_arith_rule = "simp_arith"
 val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
 val veriT_tmp_skolemize_rule = "tmp_skolemize"
-val z3_skolemize_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Skolemize
-val z3_th_lemma_rule_prefix = Z3_New_Proof.string_of_rule (Z3_New_Proof.Th_Lemma "")
+val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize
+val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "")
 val zipperposition_cnf_rule = "cnf"
 
 val skolemize_rules =
   [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule,
    spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_ite_elim_rule,

 
         val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods
 
         fun massage_methods (meths as meth :: _) =
           if not try0 then [meth]
-          else if smt_proofs = SOME true then SMT2_Method :: meths
+          else if smt_proofs = SOME true then SMT_Method :: meths
           else meths
 
         val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
         val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
         val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd

         (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed." else ""))
   end
 
 fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
   (case play of
-    Played _ => meth = SMT2_Method andalso smt_proofs <> SOME true
+    Played _ => meth = SMT_Method andalso smt_proofs <> SOME true
   | Play_Timed_Out time => Time.> (time, Time.zeroTime)
   | Play_Failed => true)
 
 fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
     (one_line_params as ((_, preplay), _, _, _)) =