# HG changeset patch
# User haftmann
# Date 1747816234 -7200
# Node ID f1c14af175919ca36b9d6f1a8c6501c005c6b2b6
# Parent  e478f85fe4274c4c9ae5681ca0d4b39ea1338668
prefer Simplifier over bootstrap-only Raw_Simplifier

diff -r e478f85fe427 -r f1c14af17591 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/FOL/simpdata.ML	Wed May 21 10:30:34 2025 +0200
@@ -82,7 +82,7 @@
   val ex_comm = @{thm ex_comm}
   val atomize =
     let val rules = @{thms atomize_all atomize_imp atomize_eq atomize_iff atomize_conj}
-    in fn ctxt => Raw_Simplifier.rewrite_wrt ctxt true rules end
+    in fn ctxt => Simplifier.rewrite_wrt ctxt true rules end
 );
 
 
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Library/conditional_parametricity.ML
--- a/src/HOL/Library/conditional_parametricity.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Library/conditional_parametricity.ML	Wed May 21 10:30:34 2025 +0200
@@ -358,7 +358,7 @@
     val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
     val prop2 = Logic.list_rename_params (rev names) prop1
     val cprop = Thm.cterm_of ctxt prop2
-    val equal_thm = Raw_Simplifier.rewrite_wrt ctxt false [Domainp_lemma] cprop
+    val equal_thm = Simplifier.rewrite_wrt ctxt false [Domainp_lemma] cprop
     fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
   in
     forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
@@ -412,7 +412,7 @@
     val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
     val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
     val cprop = Thm.cterm_of ctxt prop2
-    val equal_thm = Raw_Simplifier.rewrite_wrt ctxt false [is_equality_lemma] cprop
+    val equal_thm = Simplifier.rewrite_wrt ctxt false [is_equality_lemma] cprop
     fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
   in
     forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Library/old_recdef.ML	Wed May 21 10:30:34 2025 +0200
@@ -1230,7 +1230,7 @@
   rewrite_rule ctxt (map (fn th => th RS eq_reflection handle THM _ => th) thl);
 
 fun rew_conv ctxt ctm =
-  Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
+  Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
     (Variable.declare_term (Thm.term_of ctm) ctxt) ctm;
 
 fun simpl_conv ctxt thl ctm =
@@ -1467,7 +1467,7 @@
                      val eq = Logic.strip_imp_concl imp
                      val lhs = tych(get_lhs eq)
                      val ctxt' = Simplifier.add_prems (map ASSUME ants) ctxt
-                     val lhs_eq_lhs1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used) ctxt' lhs
+                     val lhs_eq_lhs1 = Simplifier.rewrite_cterm (false,true,false) (prover used) ctxt' lhs
                        handle Utils.ERR _ => Thm.reflexive lhs
                      val _ = print_thms ctxt' "proven:" [lhs_eq_lhs1]
                      val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
@@ -1488,7 +1488,7 @@
                   val QeqQ1 = pbeta_reduce (tych Q)
                   val Q1 = #2(Dcterm.dest_eq(cconcl QeqQ1))
                   val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt
-                  val Q1eeqQ2 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used') ctxt' Q1
+                  val Q1eeqQ2 = Simplifier.rewrite_cterm (false,true,false) (prover used') ctxt' Q1
                                 handle Utils.ERR _ => Thm.reflexive Q1
                   val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
                   val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
@@ -1513,7 +1513,7 @@
                  let val tych = Thm.cterm_of ctxt
                      val ants1 = map tych ants
                      val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt
-                     val Q_eeq_Q1 = Raw_Simplifier.rewrite_cterm
+                     val Q_eeq_Q1 = Simplifier.rewrite_cterm
                         (false,true,false) (prover used') ctxt' (tych Q)
                       handle Utils.ERR _ => Thm.reflexive (tych Q)
                      val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
@@ -1581,7 +1581,7 @@
     val ctm = Thm.cprop_of th
     val names = Misc_Legacy.add_term_names (Thm.term_of ctm, [])
     val th1 =
-      Raw_Simplifier.rewrite_cterm (false, true, false)
+      Simplifier.rewrite_cterm (false, true, false)
         (prover names) (ctxt0 addsimps [cut_lemma'] |> fold Simplifier.add_eqcong congs) ctm
     val th2 = Thm.equal_elim th1 th
  in
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Wed May 21 10:30:34 2025 +0200
@@ -18,10 +18,10 @@
 val inductive_atomize = @{thms induct_atomize};
 val inductive_rulify = @{thms induct_rulify};
 
-fun rulify_term thy = Raw_Simplifier.rewrite_term thy inductive_rulify [];
+fun rulify_term thy = Simplifier.rewrite_term thy inductive_rulify [];
 
 fun atomize_conv ctxt =
-  Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
+  Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
     (put_simpset HOL_basic_ss ctxt addsimps inductive_atomize);
 fun atomize_intr ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (atomize_conv ctxt));
 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed May 21 10:30:34 2025 +0200
@@ -19,10 +19,10 @@
 val inductive_atomize = @{thms induct_atomize};
 val inductive_rulify = @{thms induct_rulify};
 
-fun rulify_term thy = Raw_Simplifier.rewrite_term thy inductive_rulify [];
+fun rulify_term thy = Simplifier.rewrite_term thy inductive_rulify [];
 
 fun atomize_conv ctxt =
-  Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
+  Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
     (put_simpset HOL_basic_ss ctxt addsimps inductive_atomize);
 fun atomize_intr ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (atomize_conv ctxt));
 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Nonstandard_Analysis/transfer_principle.ML
--- a/src/HOL/Nonstandard_Analysis/transfer_principle.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Nonstandard_Analysis/transfer_principle.ML	Wed May 21 10:30:34 2025 +0200
@@ -74,7 +74,7 @@
     val meta = Local_Defs.meta_rewrite_rule ctxt;
     val ths' = map meta ths;
     val unfolds' = map meta unfolds and refolds' = map meta refolds;
-    val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite_wrt ctxt true unfolds' (Thm.cterm_of ctxt t))
+    val (_$_$t') = Thm.concl_of (Simplifier.rewrite_wrt ctxt true unfolds' (Thm.cterm_of ctxt t))
     val u = unstar_term consts t'
     val tac =
       rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
diff -r e478f85fe427 -r f1c14af17591 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Wed May 21 10:30:34 2025 +0200
@@ -652,7 +652,7 @@
   asm_full_simp_tac
    (Simplifier.add_simp
     @{lemma "(A & B) & C == A & B & C" by auto} (*FIXME duplicates @{thm simp_meta(3)}*)
-    (Raw_Simplifier.empty_simpset ctxt))
+    (Simplifier.empty_simpset ctxt))
   #> CHANGED
   #> REPEAT_DETERM
 
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed May 21 10:30:34 2025 +0200
@@ -1369,7 +1369,7 @@
                 rel_inject
                 |> Thm.instantiate' cTs cts
                 |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv
-                  (Raw_Simplifier.rewrite_wrt lthy false
+                  (Simplifier.rewrite_wrt lthy false
                      @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
                 |> unfold_thms lthy eq_onps
                 |> postproc
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed May 21 10:30:34 2025 +0200
@@ -519,7 +519,7 @@
     in
       @{thm asm_rl[of "\<forall>x. P x \<longrightarrow> Q x" for P Q]}
       |> Thm.instantiate' [SOME (Thm.ctyp_of \<^context> T)] []
-      |> Raw_Simplifier.rewrite_goals_rule \<^context> @{thms split_paired_All[THEN eq_reflection]}
+      |> Simplifier.rewrite_goals_rule \<^context> @{thms split_paired_All[THEN eq_reflection]}
       |> (fn thm => impI RS funpow n (fn th => allI RS th) thm)
       |> Thm.varifyT_global
     end;
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/BNF/bnf_gfp_grec.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Wed May 21 10:30:34 2025 +0200
@@ -527,7 +527,7 @@
           end);
 
     val phi =
-      Morphism.term_morphism "BNF" (Raw_Simplifier.rewrite_term (Proof_Context.theory_of lthy)
+      Morphism.term_morphism "BNF" (Simplifier.rewrite_term (Proof_Context.theory_of lthy)
         @{thms BNF_Composition.id_bnf_def} [])
       $> Morphism.thm_morphism "BNF" (unfold_thms lthy @{thms BNF_Composition.id_bnf_def});
   in
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Wed May 21 10:30:34 2025 +0200
@@ -83,8 +83,8 @@
 
 fun unfold_id_bnf_etc lthy =
   let val thy = Proof_Context.theory_of lthy in
-    Raw_Simplifier.rewrite_term thy unfold_id_thms1 []
-    #> Raw_Simplifier.rewrite_term thy @{thms BNF_Composition.id_bnf_def} []
+    Simplifier.rewrite_term thy unfold_id_thms1 []
+    #> Simplifier.rewrite_term thy @{thms BNF_Composition.id_bnf_def} []
   end;
 
 datatype corec_option =
@@ -242,7 +242,7 @@
 
     val goal = mk_Trueprop_eq (list_comb (casex, fs) $ u,
         mk_case_absumprod absT rep fs xss xss $ u')
-      |> Raw_Simplifier.rewrite_term thy @{thms comp_def[THEN eq_reflection]} [];
+      |> Simplifier.rewrite_term thy @{thms comp_def[THEN eq_reflection]} [];
     val vars = map (fst o dest_Free) (u :: fs);
 
     val dtor_ctor = nth dtor_ctors fp_res_index;
@@ -553,7 +553,7 @@
         unfold_thms_tac ctxt simps THEN HEADGOAL (rtac ctxt rho_transfer')))
       |> Thm.close_derivation \<^here>;
 
-    val goal' = Raw_Simplifier.rewrite_term thy simps [] goal;
+    val goal' = Simplifier.rewrite_term thy simps [] goal;
   in
     if null abs_rep_transfers then (goal', derive_unprimed #> fold_rho)
     else (goal, fold_rho)
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML	Wed May 21 10:30:34 2025 +0200
@@ -133,7 +133,7 @@
     val simp_ctxt = (ctxt
         |> Context_Position.set_visible false
         |> put_simpset (simpset_of (Proof_Context.init_global \<^theory>\<open>Main\<close>))
-        |> Raw_Simplifier.add_cong @{thm if_cong})
+        |> Simplifier.add_cong @{thm if_cong})
       addsimps pre_map_def :: abs_inverse :: fp_map_ident :: dtor_ctor :: rho_def ::
         @{thm convol_def} :: fpsig_nesting_map_ident0s @ fpsig_nesting_map_comps @
         fpsig_nesting_map_thms @ live_nesting_map_ident0s @ ctr_defs @ disc_sel_eq_cases' @
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Wed May 21 10:30:34 2025 +0200
@@ -79,7 +79,7 @@
     etac ctxt disjE))));
 
 fun ss_fst_snd_conv ctxt =
-  Raw_Simplifier.simpset_of (ss_only @{thms fst_conv snd_conv} ctxt);
+  Simplifier.simpset_of (ss_only @{thms fst_conv snd_conv} ctxt);
 
 fun case_atac ctxt =
   Simplifier.full_simp_tac (put_simpset (ss_fst_snd_conv ctxt) ctxt);
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Wed May 21 10:30:34 2025 +0200
@@ -37,12 +37,12 @@
   branches: scheme_branch list,
   cases: scheme_case list}
 
-fun ind_atomize ctxt = Raw_Simplifier.rewrite_wrt ctxt true @{thms induct_atomize}
-fun ind_rulify ctxt = Raw_Simplifier.rewrite_wrt ctxt true @{thms induct_rulify}
+fun ind_atomize ctxt = Simplifier.rewrite_wrt ctxt true @{thms induct_atomize}
+fun ind_rulify ctxt = Simplifier.rewrite_wrt ctxt true @{thms induct_rulify}
 
 fun meta thm = thm RS eq_reflection
 
-fun sum_prod_conv ctxt = Raw_Simplifier.rewrite_wrt ctxt true
+fun sum_prod_conv ctxt = Simplifier.rewrite_wrt ctxt true
   (map meta (@{thm split_conv} :: @{thms sum.case}))
 
 fun term_conv ctxt cv t =
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Wed May 21 10:30:34 2025 +0200
@@ -178,7 +178,7 @@
        THEN Simplifier.full_simp_tac (put_simpset curry_uncurry_ss ctxt) 5) (* simplify induction step *)
     |> (fn thm => thm OF [mono_thm, f_def])
     |> Conv.fconv_rule (Conv.concl_conv ~1    (* simplify conclusion *)
-         (Raw_Simplifier.rewrite_wrt ctxt false [mk_meta_eq @{thm Product_Type.curry_case_prod}]))
+         (Simplifier.rewrite_wrt ctxt false [mk_meta_eq @{thm Product_Type.curry_case_prod}]))
     |> singleton (Variable.export ctxt' ctxt)
   end
 
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed May 21 10:30:34 2025 +0200
@@ -196,7 +196,7 @@
         Conv.fconv_rule
           ((Conv.concl_conv (Thm.nprems_of inst_thm) o
             HOLogic.Trueprop_conv o Conv.fun2_conv o Conv.arg1_conv)
-            (Raw_Simplifier.rewrite_wrt ctxt false (Transfer.get_sym_relator_eq ctxt))) inst_thm
+            (Simplifier.rewrite_wrt ctxt false (Transfer.get_sym_relator_eq ctxt))) inst_thm
       end
 
     fun inst_relcomppI ctxt ant1 ant2 =
@@ -629,7 +629,7 @@
     val rty_forced = (domain_type o fastype_of) rsp_rel;
     val forced_rhs = force_rty_type ctxt rty_forced rhs;
     val cr_to_pcr_conv = HOLogic.Trueprop_conv (Conv.fun2_conv
-      (Raw_Simplifier.rewrite_wrt ctxt false (get_cr_pcr_eqs ctxt)))
+      (Simplifier.rewrite_wrt ctxt false (get_cr_pcr_eqs ctxt)))
     val (prsp_tm, rsp_prsp_eq) = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
       |> Thm.cterm_of ctxt
       |> cr_to_pcr_conv
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Wed May 21 10:30:34 2025 +0200
@@ -418,7 +418,7 @@
          rtac ctxt unfold_lift_sel_rsp THEN'
          case_tac exhaust_rule ctxt THEN_ALL_NEW (
         EVERY' [hyp_subst_tac ctxt, (* does not kill wits because = was rewritten to eq_onp top *)
-        Raw_Simplifier.rewrite_goal_tac ctxt (map safe_mk_meta_eq dt_rules), 
+        Simplifier.rewrite_goal_tac ctxt (map safe_mk_meta_eq dt_rules), 
         REPEAT_DETERM o etac ctxt conjE, assume_tac ctxt])) i
     val pred_simps = Transfer.lookup_pred_data lthy5 (Tname rty) |> the |> Transfer.pred_simps
     val sel_tac = lift_sel_tac (#exhaust ctr_sugar) (#case_thms ctr_sugar @ pred_simps)
@@ -439,7 +439,7 @@
       EVERY' [ SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms type_definition_def}),
         DETERM o Transfer.transfer_tac true ctxt,
           SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms eq_onp_top_eq_eq}) (* normalize *), 
-          Raw_Simplifier.rewrite_goal_tac ctxt 
+          Simplifier.rewrite_goal_tac ctxt 
           (map safe_mk_meta_eq @{thms id_apply simp_thms Ball_def}),
          rtac ctxt TrueI] i;
 
@@ -515,7 +515,7 @@
         in
           EVERY' [Transfer.gen_frees_tac [] ctxt, DETERM o (Transfer.transfer_tac true ctxt),
             case_tac exhaust ctxt THEN_ALL_NEW EVERY' [hyp_subst_tac ctxt,
-              Raw_Simplifier.rewrite_goal_tac ctxt simp_rules, rtac ctxt TrueI ]] i
+              Simplifier.rewrite_goal_tac ctxt simp_rules, rtac ctxt TrueI ]] i
         end
     end
     
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed May 21 10:30:34 2025 +0200
@@ -955,7 +955,7 @@
     val Tcon = datatype_name_of_case_name thy case_name
     val th = instantiated_case_rewrite thy Tcon
   in
-    Raw_Simplifier.rewrite_term thy [th RS @{thm eq_reflection}] [] t
+    Simplifier.rewrite_term thy [th RS @{thm eq_reflection}] [] t
   end
 
 
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed May 21 10:30:34 2025 +0200
@@ -97,7 +97,7 @@
       (Const (\<^const_name>\<open>If\<close>, _)) =>
         let
           val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
-          val atom' = Raw_Simplifier.rewrite_term thy
+          val atom' = Simplifier.rewrite_term thy
             (map (fn th => th RS @{thm eq_reflection}) [@{thm if_bool_eq_disj}, if_beta]) [] atom
           val _ = \<^assert> (not (atom = atom'))
         in
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/SMT/cvc5_replay.ML
--- a/src/HOL/Tools/SMT/cvc5_replay.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/SMT/cvc5_replay.ML	Wed May 21 10:30:34 2025 +0200
@@ -40,14 +40,14 @@
     (Lethe_Proof.Lethe_Replay_Node {id, rule, concl, bounds, declarations = decls, ...}) =
   let
     val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
-        Raw_Simplifier.rewrite_term thy rewrite_rules []
+        Simplifier.rewrite_term thy rewrite_rules []
         #> not (null ll_defs andalso Lethe_Proof.keep_raw_lifting rule) ? SMTLIB_Isar.unlift_term ll_defs
       end
     val rewrite_concl = if Lethe_Proof.keep_app_symbols rule then
           filter (curry Term.could_unify (Thm.concl_of @{thm SMT.fun_app_def}) o Thm.concl_of) rewrite_rules
         else rewrite_rules
     val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
-        Raw_Simplifier.rewrite_term thy rewrite_concl []
+        Simplifier.rewrite_term thy rewrite_concl []
         #> Object_Logic.atomize_term ctxt
         #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
         #> SMTLIB_Isar.unskolemize_names ctxt
@@ -112,7 +112,7 @@
        (ListPair.zip (map Free fixes, map Free (ListPair.zip (names, map snd fixes))))
 
     val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
-        Raw_Simplifier.rewrite_term thy ((if Lethe_Proof.keep_raw_lifting rule andalso not (null rewrite_rules) then tl rewrite_rules else rewrite_rules)) []
+        Simplifier.rewrite_term thy ((if Lethe_Proof.keep_raw_lifting rule andalso not (null rewrite_rules) then tl rewrite_rules else rewrite_rules)) []
         #> Object_Logic.atomize_term ctxt
         #> not (null ll_defs andalso Lethe_Proof.keep_raw_lifting rule) ? SMTLIB_Isar.unlift_term ll_defs
         #> SMTLIB_Isar.unskolemize_names ctxt
@@ -180,7 +180,7 @@
     val (proofs, stats, ctxt, concl_tranformation, global_transformation) = state
     val global_transformer = subst_only_free global_transformation
     val rewrite = let val thy = Proof_Context.theory_of ctxt in
-        Raw_Simplifier.rewrite_term thy (rewrite_rules) []
+        Simplifier.rewrite_term thy (rewrite_rules) []
         #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
       end
     val start0 = Timing.start ()
@@ -216,7 +216,7 @@
 fun replay_assumed assms ll_defs rewrite_rules stats ctxt term =
   let
     val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
-        Raw_Simplifier.rewrite_term thy rewrite_rules []
+        Simplifier.rewrite_term thy rewrite_rules []
         #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
       end
     val replay = Timing.timing (SMT_Replay_Methods.prove ctxt (rewrite term))
@@ -299,7 +299,7 @@
               prems = [],
               proof_ctxt = [],
               concl = Thm.prop_of th'
-                |> Raw_Simplifier.rewrite_term (Proof_Context.theory_of
+                |> Simplifier.rewrite_term (Proof_Context.theory_of
                      (empty_simpset ctxt addsimps rewrite_rules)) rewrite_rules [],
               bounds = [],
               insts = Symtab.empty,
@@ -310,7 +310,7 @@
 
     val used_assert_ids = fold add_used_asserts_in_step actual_steps []
     fun normalize_tac ctxt = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
-      Raw_Simplifier.rewrite_term thy rewrite_rules [] end
+      Simplifier.rewrite_term thy rewrite_rules [] end
     val used_assm_js =
       map_filter (fn (id, th) => let val i = index_of_id id in if i >= 0 then SOME (i, th)
           else NONE end)
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/SMT/cvc_proof_parse.ML
--- a/src/HOL/Tools/SMT/cvc_proof_parse.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/SMT/cvc_proof_parse.ML	Wed May 21 10:30:34 2025 +0200
@@ -38,7 +38,7 @@
        #> Thm.eta_long_conversion
        #> Thm.prop_of
        #> snd o Logic.dest_equals
-       #> Raw_Simplifier.rewrite_term (Proof_Context.theory_of
+       #> Simplifier.rewrite_term (Proof_Context.theory_of
           (empty_simpset ctxt addsimps rewrite_rules (*@ @{thms eq_True} still useful?*))) rewrite_rules []
 
 
@@ -47,7 +47,7 @@
        #> Thm.eta_long_conversion
        #> Thm.prop_of
        #> snd o Logic.dest_equals
-       #> Raw_Simplifier.rewrite_term (Proof_Context.theory_of
+       #> Simplifier.rewrite_term (Proof_Context.theory_of
           (empty_simpset ctxt addsimps rewrite_rules @ @{thms eq_True})) rewrite_rules []
   in (expand th) aconv (normalize th') end
 
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/SMT/lethe_replay_methods.ML
--- a/src/HOL/Tools/SMT/lethe_replay_methods.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/SMT/lethe_replay_methods.ML	Wed May 21 10:30:34 2025 +0200
@@ -991,7 +991,7 @@
       |> empty_simpset
       |> put_simpset HOL_basic_ss
       |> (fn ctxt => ctxt addsimps thms @ @{thms if_True if_False refl simp_thms if_cancel})
-      |> Raw_Simplifier.add_eqcong @{thm verit_ite_if_cong}
+      |> Simplifier.add_eqcong @{thm verit_ite_if_cong}
       |> Simplifier.full_simp_tac
   in
     SMT_Replay_Methods.prove ctxt t (fn _ => simplify_ite ctxt []
@@ -1128,7 +1128,7 @@
     ctxt
     |> empty_simpset
     |> put_simpset HOL_basic_ss
-    |> Raw_Simplifier.add_eqcong @{thm eq_reflection[OF imp_cong]}
+    |> Simplifier.add_eqcong @{thm eq_reflection[OF imp_cong]}
     |> (fn ctxt => ctxt addsimps thms addsimps @{thms simp_thms})
     |> Simplifier.full_simp_tac
 
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed May 21 10:30:34 2025 +0200
@@ -257,7 +257,7 @@
   Thm.forall_intr_vars #>
   Conv.fconv_rule (gen_normalize1_conv ctxt) #>
   (* Z3 4.3.1 silently normalizes "P --> Q --> R" to "P & Q --> R" *)
-  Raw_Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]}
+  Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]}
 
 fun gen_norm1_safe ctxt (i, thm) =
   (case try (gen_normalize1 ctxt) thm of
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/SMT/smtlib_isar.ML
--- a/src/HOL/Tools/SMT/smtlib_isar.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/SMT/smtlib_isar.ML	Wed May 21 10:30:34 2025 +0200
@@ -43,7 +43,7 @@
 
 fun postprocess_step_conclusion ctxt rewrite_rules ll_defs =
   let val thy = Proof_Context.theory_of ctxt in
-    Raw_Simplifier.rewrite_term thy rewrite_rules []
+    Simplifier.rewrite_term thy rewrite_rules []
     #> Object_Logic.atomize_term ctxt
     #> not (null ll_defs) ? unlift_term ll_defs
     #> simplify_bool
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/SMT/verit_replay.ML
--- a/src/HOL/Tools/SMT/verit_replay.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/SMT/verit_replay.ML	Wed May 21 10:30:34 2025 +0200
@@ -45,14 +45,14 @@
   let
     val _ = SMT_Config.verit_msg ctxt (fn () => \<^print> id)
     val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
-        Raw_Simplifier.rewrite_term thy rewrite_rules []
+        Simplifier.rewrite_term thy rewrite_rules []
         #> not (null ll_defs andalso Lethe_Proof.keep_raw_lifting rule) ? SMTLIB_Isar.unlift_term ll_defs
       end
     val rewrite_concl = if Lethe_Proof.keep_app_symbols rule then
           filter (curry Term.could_unify (Thm.concl_of @{thm SMT.fun_app_def}) o Thm.concl_of) rewrite_rules
         else rewrite_rules
     val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
-        Raw_Simplifier.rewrite_term thy rewrite_concl []
+        Simplifier.rewrite_term thy rewrite_concl []
         #> Object_Logic.atomize_term ctxt
         #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
         #> SMTLIB_Isar.unskolemize_names ctxt
@@ -104,7 +104,7 @@
        (ListPair.zip (map Free fixes, map Free (ListPair.zip (names, map snd fixes))))
 
     val post = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
-        Raw_Simplifier.rewrite_term thy ((if Lethe_Proof.keep_raw_lifting rule then tl rewrite_rules else rewrite_rules)) []
+        Simplifier.rewrite_term thy ((if Lethe_Proof.keep_raw_lifting rule then tl rewrite_rules else rewrite_rules)) []
         #> Object_Logic.atomize_term ctxt
         #> not (null ll_defs andalso Lethe_Proof.keep_raw_lifting rule) ? SMTLIB_Isar.unlift_term ll_defs
         #> SMTLIB_Isar.unskolemize_names ctxt
@@ -161,7 +161,7 @@
     val (proofs, stats, ctxt, concl_tranformation, global_transformation) = state
     val global_transformer = subst_only_free global_transformation
     val rewrite = let val thy = Proof_Context.theory_of ctxt in
-        Raw_Simplifier.rewrite_term thy (rewrite_rules) []
+        Simplifier.rewrite_term thy (rewrite_rules) []
         #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
       end
     val start0 = Timing.start ()
@@ -197,7 +197,7 @@
 fun replay_assumed assms ll_defs rewrite_rules stats ctxt term =
   let
     val rewrite = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
-        Raw_Simplifier.rewrite_term thy rewrite_rules []
+        Simplifier.rewrite_term thy rewrite_rules []
         #> not (null ll_defs) ? SMTLIB_Isar.unlift_term ll_defs
       end
     val replay = Timing.timing (SMT_Replay_Methods.prove ctxt (rewrite term))
@@ -243,7 +243,7 @@
         prems = [],
         proof_ctxt = [],
         concl = Thm.prop_of th
-          |> Raw_Simplifier.rewrite_term (Proof_Context.theory_of
+          |> Simplifier.rewrite_term (Proof_Context.theory_of
                (empty_simpset ctxt addsimps rewrite_rules)) rewrite_rules [],
         bounds = [],
         insts = Symtab.empty,
@@ -251,7 +251,7 @@
         subproof = ([], [], [], [])}
     val used_assert_ids = fold add_used_asserts_in_step actual_steps []
     fun normalize_tac ctxt = let val thy = Proof_Context.theory_of (empty_simpset ctxt) in
-      Raw_Simplifier.rewrite_term thy rewrite_rules [] end
+      Simplifier.rewrite_term thy rewrite_rules [] end
     val used_assm_js =
       map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME (i, nth assms i)
           else NONE end)
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML	Wed May 21 10:30:34 2025 +0200
@@ -246,7 +246,7 @@
     val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
     val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
     val cprop = Thm.cterm_of ctxt prop2
-    val equal_thm = Raw_Simplifier.rewrite_wrt ctxt false @{thms is_equality_lemma} cprop
+    val equal_thm = Simplifier.rewrite_wrt ctxt false @{thms is_equality_lemma} cprop
     fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
   in
     forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
@@ -333,7 +333,7 @@
     val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
     val prop2 = Logic.list_rename_params (rev names) prop1
     val cprop = Thm.cterm_of ctxt prop2
-    val equal_thm = Raw_Simplifier.rewrite_wrt ctxt false @{thms Domainp_lemma} cprop
+    val equal_thm = Simplifier.rewrite_wrt ctxt false @{thms Domainp_lemma} cprop
     fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
   in
     forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
@@ -693,7 +693,7 @@
       |> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
     val thm2 = thm1
       |> Thm.instantiate (TVars.make instT, Vars.empty)
-      |> Raw_Simplifier.rewrite_rule ctxt pre_simps
+      |> Simplifier.rewrite_rule ctxt pre_simps
     val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
     val rule = transfer_rule_of_lhs ctxt' (HOLogic.dest_Trueprop (Thm.concl_of thm2))
   in
@@ -707,7 +707,7 @@
               THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
           handle TERM (_, ts) =>
             raise TERM ("Transfer failed to convert goal to an object-logic formula", ts))
-    |> Raw_Simplifier.rewrite_rule ctxt' post_simps
+    |> Simplifier.rewrite_rule ctxt' post_simps
     |> Simplifier.norm_hhf ctxt'
     |> Drule.generalize
         (Names.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Names.empty)
@@ -728,7 +728,7 @@
       |> map (fn v as ((a, _), S) => (v, Thm.ctyp_of ctxt (TFree (a, S))))
     val thm2 = thm1
       |> Thm.instantiate (TVars.make instT, Vars.empty)
-      |> Raw_Simplifier.rewrite_rule ctxt pre_simps
+      |> Simplifier.rewrite_rule ctxt pre_simps
     val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt
     val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)
     val rule = transfer_rule_of_term ctxt' true t
@@ -743,7 +743,7 @@
               THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1
           handle TERM (_, ts) =>
             raise TERM ("Transfer failed to convert goal to an object-logic formula", ts))
-    |> Raw_Simplifier.rewrite_rule ctxt' post_simps
+    |> Simplifier.rewrite_rule ctxt' post_simps
     |> Simplifier.norm_hhf ctxt'
     |> Drule.generalize
         (Names.make_set (map (fst o dest_TFree o Thm.typ_of o snd) instT), Names.empty)
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed May 21 10:30:34 2025 +0200
@@ -333,7 +333,7 @@
 
 val bad_app = "Inductive predicate must be applied to parameter(s) ";
 
-fun atomize_term thy = Raw_Simplifier.rewrite_term thy inductive_atomize [];
+fun atomize_term thy = Simplifier.rewrite_term thy inductive_atomize [];
 
 in
 
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/nat_arith.ML
--- a/src/HOL/Tools/nat_arith.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/nat_arith.ML	Wed May 21 10:30:34 2025 +0200
@@ -19,7 +19,7 @@
 
 fun move_to_front ctxt path = Conv.every_conv
     [Conv.rewr_conv (Library.foldl (op RS) (@{thm nat_arith.rule0}, path)),
-     Conv.arg_conv (Raw_Simplifier.rewrite_wrt ctxt false norm_rules)]
+     Conv.arg_conv (Simplifier.rewrite_wrt ctxt false norm_rules)]
 
 fun add_atoms path \<^Const_>\<open>plus _ for x y\<close> =
       add_atoms (@{thm nat_arith.add1}::path) x #>
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Wed May 21 10:30:34 2025 +0200
@@ -438,7 +438,7 @@
     val (t', ctxt') = yield_singleton (Variable.import_terms true) t (Variable.declare_term t ctxt)
     val ct = Thm.cterm_of ctxt' t'
     fun unfold_conv thms =
-      Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
+      Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
         (empty_simpset ctxt' addsimps thms)
     val prep_eq = (comprehension_conv ctxt' then_conv unfold_conv prep_thms) ct
     val t'' = Thm.term_of (Thm.rhs_of prep_eq)
@@ -476,7 +476,7 @@
 fun code_proc ctxt redex =
   let
     fun unfold_conv thms =
-      Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
+      Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
         (empty_simpset ctxt addsimps thms)
     val prep_thm = unfold_conv @{thms eq_equal[symmetric]} redex
   in
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Tools/simpdata.ML	Wed May 21 10:30:34 2025 +0200
@@ -35,7 +35,7 @@
   val ex_comm = @{thm ex_comm}
   val atomize =
     let val rules = @{thms atomize_all atomize_imp atomize_eq atomize_conj}
-    in fn ctxt => Raw_Simplifier.rewrite_wrt ctxt true rules end
+    in fn ctxt => Simplifier.rewrite_wrt ctxt true rules end
 );
 
 structure Simpdata =
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Types_To_Sets/Examples/Prerequisites.thy
--- a/src/HOL/Types_To_Sets/Examples/Prerequisites.thy	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Types_To_Sets/Examples/Prerequisites.thy	Wed May 21 10:30:34 2025 +0200
@@ -79,7 +79,7 @@
   end
 
 fun var_simplify_only ctxt ths thm =
-  asm_full_var_simplify (Raw_Simplifier.clear_simpset ctxt addsimps ths) thm
+  asm_full_var_simplify (Simplifier.clear_simpset ctxt addsimps ths) thm
 
 val var_simplified = Attrib.thms >>
   (fn ths => Thm.rule_attribute ths
diff -r e478f85fe427 -r f1c14af17591 src/HOL/Types_To_Sets/unoverload_type.ML
--- a/src/HOL/Types_To_Sets/unoverload_type.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Wed May 21 10:30:34 2025 +0200
@@ -47,7 +47,7 @@
         |> map varify_const
     in
       fold Unoverloading.unoverload consts thm''
-      |> Raw_Simplifier.norm_hhf (Context.proof_of context)
+      |> Simplifier.norm_hhf (Context.proof_of context)
     end
   end
 
diff -r e478f85fe427 -r f1c14af17591 src/Pure/ex/Guess.thy
--- a/src/Pure/ex/Guess.thy	Wed May 21 10:30:33 2025 +0200
+++ b/src/Pure/ex/Guess.thy	Wed May 21 10:30:34 2025 +0200
@@ -152,7 +152,7 @@
         ctxt' (k, [(s, [th])]);
     val before_qed =
       Method.primitive_text (fn ctxt =>
-        Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #>
+        Goal.conclude #> Simplifier.norm_hhf ctxt #>
           (fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th)));
     fun after_qed (result_ctxt, results) state' =
       let
diff -r e478f85fe427 -r f1c14af17591 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/Pure/simplifier.ML	Wed May 21 10:30:34 2025 +0200
@@ -157,10 +157,10 @@
 (* simproc_setup with concrete syntax *)
 
 val simproc_setup =
-  Named_Target.setup_result Raw_Simplifier.transform_simproc o define_simproc;
+  Named_Target.setup_result transform_simproc o define_simproc;
 
 fun simproc_setup_cmd args =
-  Named_Target.setup_result Raw_Simplifier.transform_simproc
+  Named_Target.setup_result transform_simproc
     (fn lthy => lthy |> define_simproc (read_simproc_spec lthy args));
 
 val parse_proc_kind =
@@ -310,20 +310,20 @@
 
 fun solve_all_tac solvers ctxt =
   let
-    val subgoal_tac = Raw_Simplifier.subgoal_tac (Raw_Simplifier.set_solvers solvers ctxt);
+    val subgoal_tac = subgoal_tac (set_solvers solvers ctxt);
     val solve_tac = subgoal_tac THEN_ALL_NEW (K no_tac);
   in DEPTH_SOLVE (solve_tac 1) end;
 
 (*NOTE: may instantiate unknowns that appear also in other subgoals*)
 fun generic_simp_tac safe mode ctxt =
   let
-    val loop_tac = Raw_Simplifier.loop_tac ctxt;
-    val (unsafe_solvers, solvers) = Raw_Simplifier.solvers ctxt;
-    val solve_tac = FIRST' (map (Raw_Simplifier.solver ctxt)
+    val loop_tac = loop_tac ctxt;
+    val (unsafe_solvers, solvers) = solvers ctxt;
+    val solve_tac = FIRST' (map (solver ctxt)
       (rev (if safe then solvers else unsafe_solvers)));
 
     fun simp_loop_tac i =
-      Raw_Simplifier.generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ctxt i THEN
+      generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ctxt i THEN
       (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
   in PREFER_GOAL (simp_loop_tac 1) end;
 
@@ -331,15 +331,15 @@
 
 fun simp rew mode ctxt thm =
   let
-    val (unsafe_solvers, _) = Raw_Simplifier.solvers ctxt;
+    val (unsafe_solvers, _) = solvers ctxt;
     val tacf = solve_all_tac (rev unsafe_solvers);
     fun prover s th = Option.map #1 (Seq.pull (tacf s th));
   in rew mode prover ctxt thm end;
 
 in
 
-val simp_thm = simp Raw_Simplifier.rewrite_thm;
-val simp_cterm = simp Raw_Simplifier.rewrite_cterm;
+val simp_thm = simp rewrite_thm;
+val simp_cterm = simp rewrite_cterm;
 
 end;
 
@@ -398,7 +398,7 @@
   (Args.del -- Args.colon >> K del_proc ||
     Scan.option (Args.add -- Args.colon) >> K add_proc)
   >> (fn f => fn simproc => Morphism.entity (fn phi => Thm.declaration_attribute
-      (K (Raw_Simplifier.map_ss (f (transform_simproc phi simproc))))));
+      (K (map_ss (f (transform_simproc phi simproc))))));
 
 in
 
@@ -425,7 +425,7 @@
 
 val simplified = conv_mode -- Attrib.thms >>
   (fn (f, ths) => Thm.rule_attribute ths (fn context =>
-    f ((if null ths then I else Raw_Simplifier.clear_simpset)
+    f ((if null ths then I else clear_simpset)
         (Context.proof_of context) addsimps ths)));
 
 end;
@@ -460,7 +460,7 @@
   Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
   Args.$$$ simpN -- Args.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>),
   Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >>
-    K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
+    K {init = clear_simpset, attribute = simp_add, pos = \<^here>}]
    @ cong_modifiers;
 
 val simp_modifiers' =
@@ -468,7 +468,7 @@
   Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
   Args.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>),
   Args.$$$ onlyN -- Args.colon >>
-    K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
+    K {init = clear_simpset, attribute = simp_add, pos = \<^here>}]
    @ cong_modifiers;
 
 val simp_options =
@@ -500,12 +500,12 @@
     "simplification (all goals)";
 
 fun unsafe_solver_tac ctxt =
-  FIRST' [resolve_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), assume_tac ctxt];
+  FIRST' [resolve_tac ctxt (Drule.reflexive_thm :: prems_of ctxt), assume_tac ctxt];
 val unsafe_solver = mk_solver "Pure unsafe" unsafe_solver_tac;
 
 (*no premature instantiation of variables during simplification*)
 fun safe_solver_tac ctxt =
-  FIRST' [match_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), eq_assume_tac];
+  FIRST' [match_tac ctxt (Drule.reflexive_thm :: prems_of ctxt), eq_assume_tac];
 val safe_solver = mk_solver "Pure safe" safe_solver_tac;
 
 val _ =
diff -r e478f85fe427 -r f1c14af17591 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/Tools/Code/code_runtime.ML	Wed May 21 10:30:34 2025 +0200
@@ -362,7 +362,7 @@
 fun preprocess_conv { ctxt } = 
   let
     val rules = get ctxt;
-  in fn ctxt' => Raw_Simplifier.rewrite_wrt ctxt' false rules end;
+  in fn ctxt' => Simplifier.rewrite_wrt ctxt' false rules end;
 
 fun preprocess_term { ctxt } =
   let
diff -r e478f85fe427 -r f1c14af17591 src/Tools/atomize_elim.ML
--- a/src/Tools/atomize_elim.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/Tools/atomize_elim.ML	Wed May 21 10:30:34 2025 +0200
@@ -54,7 +54,7 @@
 *)
 fun atomize_elim_conv ctxt ct =
     (forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt
-    then_conv Raw_Simplifier.rewrite_wrt ctxt true (Named_Theorems.get ctxt named_theorems)
+    then_conv Simplifier.rewrite_wrt ctxt true (Named_Theorems.get ctxt named_theorems)
     then_conv (fn ct' => if can (Object_Logic.dest_judgment ctxt) ct'
                          then all_conv ct'
                          else raise CTERM ("atomize_elim", [ct', ct])))
diff -r e478f85fe427 -r f1c14af17591 src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/Tools/coherent.ML	Wed May 21 10:30:34 2025 +0200
@@ -42,7 +42,7 @@
   if is_atomic (Logic.strip_imp_concl (Thm.term_of ct)) then Conv.all_conv ct
   else Conv.concl_conv (length (Logic.strip_imp_prems (Thm.term_of ct)))
     (Conv.rewr_conv (Thm.symmetric Data.atomize_elimL) then_conv
-     Raw_Simplifier.rewrite_wrt ctxt true (map Thm.symmetric
+     Simplifier.rewrite_wrt ctxt true (map Thm.symmetric
        [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
 
 fun rulify_elim ctxt th = Simplifier.norm_hhf ctxt (Conv.fconv_rule (rulify_elim_conv ctxt) th);
diff -r e478f85fe427 -r f1c14af17591 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/Tools/induct.ML	Wed May 21 10:30:34 2025 +0200
@@ -442,10 +442,10 @@
 
 fun mark_constraints n ctxt = Conv.fconv_rule
   (Conv.prems_conv ~1 (Conv.params_conv ~1 (fn ctxt' =>
-      Conv.prems_conv n (Raw_Simplifier.rewrite_wrt ctxt' false [equal_def'])) ctxt));
+      Conv.prems_conv n (Simplifier.rewrite_wrt ctxt' false [equal_def'])) ctxt));
 
 fun unmark_constraints ctxt =
-  Conv.fconv_rule (Raw_Simplifier.rewrite_wrt ctxt true [Induct_Args.equal_def]);
+  Conv.fconv_rule (Simplifier.rewrite_wrt ctxt true [Induct_Args.equal_def]);
 
 
 (* simplify *)
@@ -546,10 +546,10 @@
 (* atomize *)
 
 fun atomize_term ctxt =
-  Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) Induct_Args.atomize []
+  Simplifier.rewrite_term (Proof_Context.theory_of ctxt) Induct_Args.atomize []
   #> Object_Logic.drop_judgment ctxt;
 
-fun atomize_cterm ctxt = Raw_Simplifier.rewrite_wrt ctxt true Induct_Args.atomize;
+fun atomize_cterm ctxt = Simplifier.rewrite_wrt ctxt true Induct_Args.atomize;
 
 fun atomize_tac ctxt = rewrite_goal_tac ctxt Induct_Args.atomize;
 
@@ -560,8 +560,8 @@
 (* rulify *)
 
 fun rulify_term thy =
-  Raw_Simplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #>
-  Raw_Simplifier.rewrite_term thy Induct_Args.rulify_fallback [];
+  Simplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #>
+  Simplifier.rewrite_term thy Induct_Args.rulify_fallback [];
 
 fun rulified_term ctxt thm =
   let
@@ -702,7 +702,7 @@
 fun miniscope_tac p =
   CONVERSION o
     Conv.params_conv p (fn ctxt =>
-      Raw_Simplifier.rewrite_wrt ctxt true [Thm.symmetric Drule.norm_hhf_eq]);
+      Simplifier.rewrite_wrt ctxt true [Thm.symmetric Drule.norm_hhf_eq]);
 
 in