# HG changeset patch
# User haftmann
# Date 1747816207 -7200
# Node ID d22294b20573fadbb225b0b8e573e24bf8bf8ac5
# Parent  9e35c1662aecc172163140d97ce1880c4fce31a1
disambiguate function name wrt. structures Simplifier vs. Raw_Simplifier

diff -r 9e35c1662aec -r d22294b20573 NEWS
--- a/NEWS	Wed May 21 10:30:06 2025 +0200
+++ b/NEWS	Wed May 21 10:30:07 2025 +0200
@@ -72,6 +72,9 @@
 * Command 'thy_deps' expects optional theory arguments as long theory names,
 the same way as the 'imports' clause. Minor INCOMPATIBILITY.
 
+* ML function 'Raw_Simplifier.rewrite' renamed to 'Raw_Simplifier.rewrite_wrt',
+to avoid clash with existing 'Simplifier.rewrite'. INCOMPATIBILITY.
+
 
 *** HOL ***
 
diff -r 9e35c1662aec -r d22294b20573 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/FOL/simpdata.ML	Wed May 21 10:30:07 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 ctxt true rules end
+    in fn ctxt => Raw_Simplifier.rewrite_wrt ctxt true rules end
 );
 
 
diff -r 9e35c1662aec -r d22294b20573 src/HOL/Library/conditional_parametricity.ML
--- a/src/HOL/Library/conditional_parametricity.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/HOL/Library/conditional_parametricity.ML	Wed May 21 10:30:07 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 ctxt false [Domainp_lemma] cprop
+    val equal_thm = Raw_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 ctxt false [is_equality_lemma] cprop
+    val equal_thm = Raw_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 9e35c1662aec -r d22294b20573 src/HOL/Nonstandard_Analysis/transfer_principle.ML
--- a/src/HOL/Nonstandard_Analysis/transfer_principle.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/HOL/Nonstandard_Analysis/transfer_principle.ML	Wed May 21 10:30:07 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 ctxt true unfolds' (Thm.cterm_of ctxt t))
+    val (_$_$t') = Thm.concl_of (Raw_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 9e35c1662aec -r d22294b20573 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed May 21 10:30:07 2025 +0200
@@ -1369,7 +1369,7 @@
                 rel_inject
                 |> Thm.instantiate' cTs cts
                 |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv
-                  (Raw_Simplifier.rewrite lthy false
+                  (Raw_Simplifier.rewrite_wrt lthy false
                      @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
                 |> unfold_thms lthy eq_onps
                 |> postproc
diff -r 9e35c1662aec -r d22294b20573 src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Wed May 21 10:30:07 2025 +0200
@@ -37,12 +37,12 @@
   branches: scheme_branch list,
   cases: scheme_case list}
 
-fun ind_atomize ctxt = Raw_Simplifier.rewrite ctxt true @{thms induct_atomize}
-fun ind_rulify ctxt = Raw_Simplifier.rewrite ctxt true @{thms induct_rulify}
+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 meta thm = thm RS eq_reflection
 
-fun sum_prod_conv ctxt = Raw_Simplifier.rewrite ctxt true
+fun sum_prod_conv ctxt = Raw_Simplifier.rewrite_wrt ctxt true
   (map meta (@{thm split_conv} :: @{thms sum.case}))
 
 fun term_conv ctxt cv t =
diff -r 9e35c1662aec -r d22294b20573 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Wed May 21 10:30:07 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 ctxt false [mk_meta_eq @{thm Product_Type.curry_case_prod}]))
+         (Raw_Simplifier.rewrite_wrt ctxt false [mk_meta_eq @{thm Product_Type.curry_case_prod}]))
     |> singleton (Variable.export ctxt' ctxt)
   end
 
diff -r 9e35c1662aec -r d22294b20573 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed May 21 10:30:07 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 ctxt false (Transfer.get_sym_relator_eq ctxt))) inst_thm
+            (Raw_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 ctxt false (get_cr_pcr_eqs ctxt)))
+      (Raw_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 9e35c1662aec -r d22294b20573 src/HOL/Tools/Transfer/transfer.ML
--- a/src/HOL/Tools/Transfer/transfer.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML	Wed May 21 10:30:07 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 ctxt false @{thms is_equality_lemma} cprop
+    val equal_thm = Raw_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 ctxt false @{thms Domainp_lemma} cprop
+    val equal_thm = Raw_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}))
diff -r 9e35c1662aec -r d22294b20573 src/HOL/Tools/nat_arith.ML
--- a/src/HOL/Tools/nat_arith.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/HOL/Tools/nat_arith.ML	Wed May 21 10:30:07 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 ctxt false norm_rules)]
+     Conv.arg_conv (Raw_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 9e35c1662aec -r d22294b20573 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/HOL/Tools/simpdata.ML	Wed May 21 10:30:07 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 ctxt true rules end
+    in fn ctxt => Raw_Simplifier.rewrite_wrt ctxt true rules end
 );
 
 structure Simpdata =
diff -r 9e35c1662aec -r d22294b20573 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/Pure/Isar/local_defs.ML	Wed May 21 10:30:07 2025 +0200
@@ -168,7 +168,7 @@
   export inner outer (Drule.mk_term ct) ||> Drule.dest_term;
 
 fun contract ctxt defs ct th =
-  th COMP (Raw_Simplifier.rewrite ctxt true defs ct COMP_INCR Drule.equal_elim_rule2);
+  th COMP (Raw_Simplifier.rewrite_wrt ctxt true defs ct COMP_INCR Drule.equal_elim_rule2);
 
 
 
diff -r 9e35c1662aec -r d22294b20573 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/Pure/Isar/object_logic.ML	Wed May 21 10:30:07 2025 +0200
@@ -203,7 +203,7 @@
   drop_judgment ctxt o
     Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) (get_atomize ctxt) [];
 
-fun atomize ctxt = Raw_Simplifier.rewrite ctxt true (get_atomize ctxt);
+fun atomize ctxt = Raw_Simplifier.rewrite_wrt ctxt true (get_atomize ctxt);
 
 fun atomize_prems ctxt ct =
   if Logic.has_meta_prems (Thm.term_of ct) then
@@ -222,7 +222,7 @@
 fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify ctxt);
 
 fun gen_rulify full ctxt =
-  Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify ctxt))
+  Conv.fconv_rule (Raw_Simplifier.rewrite_wrt ctxt full (get_rulify ctxt))
   #> Variable.gen_all ctxt
   #> Thm.strip_shyps
   #> Drule.zero_var_indexes;
diff -r 9e35c1662aec -r d22294b20573 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Wed May 21 10:30:07 2025 +0200
@@ -184,14 +184,14 @@
 
 fun unfold_prems ctxt n defs th =
   if null defs then th
-  else Conv.fconv_rule (Conv.prems_conv n (Raw_Simplifier.rewrite ctxt true defs)) th;
+  else Conv.fconv_rule (Conv.prems_conv n (Raw_Simplifier.rewrite_wrt ctxt true defs)) th;
 
 fun unfold_prems_concls ctxt defs th =
   if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
   else
     Conv.fconv_rule
       (Conv.concl_conv ~1 (Conjunction.convs
-        (Conv.prems_conv ~1 (Raw_Simplifier.rewrite ctxt true defs)))) th;
+        (Conv.prems_conv ~1 (Raw_Simplifier.rewrite_wrt ctxt true defs)))) th;
 
 in
 
diff -r 9e35c1662aec -r d22294b20573 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/Pure/axclass.ML	Wed May 21 10:30:07 2025 +0200
@@ -169,8 +169,8 @@
 fun unoverload ctxt = rewrite_rule ctxt (inst_thms ctxt);
 fun overload ctxt = rewrite_rule ctxt (map Thm.symmetric (inst_thms ctxt));
 
-fun unoverload_conv ctxt = Raw_Simplifier.rewrite ctxt true (inst_thms ctxt);
-fun overload_conv ctxt = Raw_Simplifier.rewrite ctxt true (map Thm.symmetric (inst_thms ctxt));
+fun unoverload_conv ctxt = Raw_Simplifier.rewrite_wrt ctxt true (inst_thms ctxt);
+fun overload_conv ctxt = Raw_Simplifier.rewrite_wrt ctxt true (map Thm.symmetric (inst_thms ctxt));
 
 fun lookup_inst_param consts params (c, T) =
   (case get_inst_tyco consts (c, T) of
diff -r 9e35c1662aec -r d22294b20573 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/Pure/raw_simplifier.ML	Wed May 21 10:30:07 2025 +0200
@@ -117,11 +117,17 @@
   val generic_rewrite_goal_tac: bool * bool * bool ->
     (Proof.context -> tactic) -> Proof.context -> int -> tactic
   val rewrite0: Proof.context -> bool -> conv
-  val rewrite: Proof.context -> bool -> thm list -> conv
+  val rewrite_wrt: Proof.context -> bool -> thm list -> conv
   val rewrite0_rule: Proof.context -> thm -> thm
 end;
 
-structure Raw_Simplifier: RAW_SIMPLIFIER =
+signature LEGACY_RAW_SIMPLIFIER =
+sig
+  include RAW_SIMPLIFIER
+  val rewrite: Proof.context -> bool -> thm list -> conv
+end
+
+structure Raw_Simplifier: LEGACY_RAW_SIMPLIFIER =
 struct
 
 (** datatype simpset **)
@@ -1484,11 +1490,13 @@
 
 fun rewrite0 ctxt full = rewrite_cterm (full, false, false) simple_prover ctxt;
 
-fun rewrite _ _ [] = Thm.reflexive
-  | rewrite ctxt full thms = rewrite0 (init_simpset thms ctxt) full;
+fun rewrite_wrt _ _ [] = Thm.reflexive
+  | rewrite_wrt ctxt full thms = rewrite0 (init_simpset thms ctxt) full;
+
+val rewrite = rewrite_wrt;
 
 fun rewrite0_rule ctxt = Conv.fconv_rule (rewrite0 ctxt true);
-fun rewrite_rule ctxt = Conv.fconv_rule o rewrite ctxt true;
+fun rewrite_rule ctxt = Conv.fconv_rule o rewrite_wrt ctxt true;
 
 (*simple term rewriting -- no proof*)
 fun rewrite_term thy rules procs =
diff -r 9e35c1662aec -r d22294b20573 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/Tools/Code/code_runtime.ML	Wed May 21 10:30:07 2025 +0200
@@ -362,7 +362,7 @@
 fun preprocess_conv { ctxt } = 
   let
     val rules = get ctxt;
-  in fn ctxt' => Raw_Simplifier.rewrite ctxt' false rules end;
+  in fn ctxt' => Raw_Simplifier.rewrite_wrt ctxt' false rules end;
 
 fun preprocess_term { ctxt } =
   let
diff -r 9e35c1662aec -r d22294b20573 src/Tools/atomize_elim.ML
--- a/src/Tools/atomize_elim.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/Tools/atomize_elim.ML	Wed May 21 10:30:07 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 ctxt true (Named_Theorems.get ctxt named_theorems)
+    then_conv Raw_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 9e35c1662aec -r d22294b20573 src/Tools/coherent.ML
--- a/src/Tools/coherent.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/Tools/coherent.ML	Wed May 21 10:30:07 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 ctxt true (map Thm.symmetric
+     Raw_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 9e35c1662aec -r d22294b20573 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/Tools/induct.ML	Wed May 21 10:30:07 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 ctxt' false [equal_def'])) ctxt));
+      Conv.prems_conv n (Raw_Simplifier.rewrite_wrt ctxt' false [equal_def'])) ctxt));
 
 fun unmark_constraints ctxt =
-  Conv.fconv_rule (Raw_Simplifier.rewrite ctxt true [Induct_Args.equal_def]);
+  Conv.fconv_rule (Raw_Simplifier.rewrite_wrt ctxt true [Induct_Args.equal_def]);
 
 
 (* simplify *)
@@ -549,7 +549,7 @@
   Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) Induct_Args.atomize []
   #> Object_Logic.drop_judgment ctxt;
 
-fun atomize_cterm ctxt = Raw_Simplifier.rewrite ctxt true Induct_Args.atomize;
+fun atomize_cterm ctxt = Raw_Simplifier.rewrite_wrt ctxt true Induct_Args.atomize;
 
 fun atomize_tac ctxt = rewrite_goal_tac ctxt Induct_Args.atomize;
 
@@ -702,7 +702,7 @@
 fun miniscope_tac p =
   CONVERSION o
     Conv.params_conv p (fn ctxt =>
-      Raw_Simplifier.rewrite ctxt true [Thm.symmetric Drule.norm_hhf_eq]);
+      Raw_Simplifier.rewrite_wrt ctxt true [Thm.symmetric Drule.norm_hhf_eq]);
 
 in