# HG changeset patch
# User wenzelm
# Date 1723576191 -7200
# Node ID cc4ecaa8e96eb2b9b09f8fc4119dd62e786f52a6
# Parent  71910299bbcd597b2cbd8e74eacdb6d98a3f0cb6
tuned: prefer canonical argument order;

diff -r 71910299bbcd -r cc4ecaa8e96e src/Benchmarks/Record_Benchmark/Record_Benchmark.thy
--- a/src/Benchmarks/Record_Benchmark/Record_Benchmark.thy	Tue Aug 13 19:28:58 2024 +0200
+++ b/src/Benchmarks/Record_Benchmark/Record_Benchmark.thy	Tue Aug 13 21:09:51 2024 +0200
@@ -356,12 +356,12 @@
 
 lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
   apply (tactic \<open>simp_tac
-    (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.upd_simproc]) 1\<close>)
+    (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc Record.upd_simproc) 1\<close>)
   done
 
 lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
   apply (tactic \<open>simp_tac
-    (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+    (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
   apply simp
   done
 
@@ -372,7 +372,7 @@
 
 lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
   apply (tactic \<open>simp_tac
-    (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+    (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
   apply simp
   done
 
@@ -383,7 +383,7 @@
 
 lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
   apply (tactic \<open>simp_tac
-    (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+    (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
   apply auto
   done
 
@@ -417,7 +417,7 @@
 
 lemma "\<exists>r. A155 r = x"
   apply (tactic \<open>simp_tac
-    (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.ex_sel_eq_simproc]) 1\<close>)
+    (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc (Record.ex_sel_eq_simproc)) 1\<close>)
   done
 
 print_record many_A
diff -r 71910299bbcd -r cc4ecaa8e96e src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Tue Aug 13 21:09:51 2024 +0200
@@ -53,7 +53,8 @@
           div_by_1 mod_by_1 div_by_Suc_0 mod_by_Suc_0
           Suc_eq_plus1}
       addsimps @{thms ac_simps}
-      addsimprocs [\<^simproc>\<open>cancel_div_mod_nat\<close>, \<^simproc>\<open>cancel_div_mod_int\<close>]
+      |> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_nat\<close>
+      |> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_int\<close>
     val simpset0 =
       put_simpset HOL_basic_ss ctxt
       addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1 simp_thms}
diff -r 71910299bbcd -r cc4ecaa8e96e src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Tue Aug 13 21:09:51 2024 +0200
@@ -176,7 +176,7 @@
   let
     val ctxt' =
       Context_Position.set_visible false (put_simpset dlo_ss ctxt)
-        addsimps @{thms dnf_simps} addsimprocs [reduce_ex_simproc]
+        addsimps @{thms dnf_simps} |> Simplifier.add_proc reduce_ex_simproc
     val dnfex_conv = Simplifier.rewrite ctxt'
     val pcv =
       Simplifier.rewrite
diff -r 71910299bbcd -r cc4ecaa8e96e src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Tue Aug 13 21:09:51 2024 +0200
@@ -68,14 +68,16 @@
     (* Transform the term*)
     val (t,np,nh) = prepare_for_mir q g
     (* Some simpsets for dealing with mod div abs and nat*)
-    val mod_div_simpset = put_simpset HOL_basic_ss ctxt
-                        addsimps [refl, @{thm mod_add_eq}, 
-                                  @{thm mod_self},
-                                  @{thm div_0}, @{thm mod_0},
-                                  @{thm div_by_1}, @{thm mod_by_1}, @{thm div_by_Suc_0}, @{thm mod_by_Suc_0},
-                                  @{thm "Suc_eq_plus1"}]
-                        addsimps @{thms add.assoc add.commute add.left_commute}
-                        addsimprocs [\<^simproc>\<open>cancel_div_mod_nat\<close>, \<^simproc>\<open>cancel_div_mod_int\<close>]
+    val mod_div_simpset =
+      put_simpset HOL_basic_ss ctxt
+      addsimps [refl, @{thm mod_add_eq}, 
+                @{thm mod_self},
+                @{thm div_0}, @{thm mod_0},
+                @{thm div_by_1}, @{thm mod_by_1}, @{thm div_by_Suc_0}, @{thm mod_by_Suc_0},
+                @{thm "Suc_eq_plus1"}]
+      addsimps @{thms add.assoc add.commute add.left_commute}
+      |> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_nat\<close>
+      |> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_int\<close>
     val simpset0 = put_simpset HOL_basic_ss ctxt
       addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1}
       addsimps comp_ths
diff -r 71910299bbcd -r cc4ecaa8e96e src/HOL/Examples/Records.thy
--- a/src/HOL/Examples/Records.thy	Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Examples/Records.thy	Tue Aug 13 21:09:51 2024 +0200
@@ -244,7 +244,7 @@
 
 lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
   apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
-    addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+    |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
   apply simp
   done
 
@@ -255,7 +255,7 @@
 
 lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
   apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
-    addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+    |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
   apply simp
   done
 
@@ -266,7 +266,7 @@
 
 lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
   apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
-    addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+    |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
   apply auto
   done
 
diff -r 71910299bbcd -r cc4ecaa8e96e src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Aug 13 21:09:51 2024 +0200
@@ -35,7 +35,7 @@
 
 val beta_ss =
   simpset_of (put_simpset HOL_basic_ss \<^context>
-    addsimps @{thms simp_thms} addsimprocs [\<^simproc>\<open>beta_cfun_proc\<close>])
+    addsimps @{thms simp_thms} |> Simplifier.add_proc \<^simproc>\<open>beta_cfun_proc\<close>)
 
 fun is_cpo thy T = Sign.of_sort thy (T, \<^sort>\<open>cpo\<close>)
 
diff -r 71910299bbcd -r cc4ecaa8e96e src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Tue Aug 13 21:09:51 2024 +0200
@@ -108,7 +108,7 @@
 
 val beta_ss =
   simpset_of (put_simpset HOL_basic_ss \<^context>
-    addsimps @{thms simp_thms} addsimprocs [\<^simproc>\<open>beta_cfun_proc\<close>])
+    addsimps @{thms simp_thms} |> Simplifier.add_proc \<^simproc>\<open>beta_cfun_proc\<close>)
 
 (******************************************************************************)
 (******************************** theory data *********************************)
diff -r 71910299bbcd -r cc4ecaa8e96e src/HOL/Hoare/hoare_tac.ML
--- a/src/HOL/Hoare/hoare_tac.ML	Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML	Tue Aug 13 21:09:51 2024 +0200
@@ -157,7 +157,7 @@
 fun basic_simp_tac ctxt var_names tac =
   simp_tac
     (put_simpset HOL_basic_ss ctxt
-      addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [Record.simproc])
+      addsimps [mem_Collect_eq, @{thm split_conv}] |> Simplifier.add_proc Record.simproc)
   THEN_MAYBE' max_simp_tac ctxt var_names tac;
 
 
diff -r 71910299bbcd -r cc4ecaa8e96e src/HOL/Library/Cancellation/cancel.ML
--- a/src/HOL/Library/Cancellation/cancel.ML	Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Library/Cancellation/cancel.ML	Tue Aug 13 21:09:51 2024 +0200
@@ -48,9 +48,10 @@
   let
     val t = Thm.term_of ct
     val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt
-    val pre_simplified_ct = Simplifier.full_rewrite (clear_simpset ctxt addsimps
-      Named_Theorems.get ctxt \<^named_theorems>\<open>cancelation_simproc_pre\<close> addsimprocs
-      [\<^simproc>\<open>NO_MATCH\<close>]) (Thm.cterm_of ctxt t');
+    val pre_simplified_ct =
+      Simplifier.full_rewrite (clear_simpset ctxt
+        addsimps Named_Theorems.get ctxt \<^named_theorems>\<open>cancelation_simproc_pre\<close>
+        |> Simplifier.add_proc \<^simproc>\<open>NO_MATCH\<close>) (Thm.cterm_of ctxt t');
     val t' = Thm.term_of (Thm.rhs_of pre_simplified_ct)
     val export = singleton (Variable.export ctxt' ctxt)
 
@@ -66,11 +67,11 @@
     val canceled_thm = Cancel_Numerals_Fun.proc ctxt (Thm.rhs_of pre_simplified_ct)
     fun add_pre_simplification thm = @{thm Pure.transitive} OF [pre_simplified_ct, thm]
     fun add_post_simplification thm =
-      (let val post_simplified_ct = Simplifier.full_rewrite (clear_simpset ctxt addsimps
-              Named_Theorems.get ctxt \<^named_theorems>\<open>cancelation_simproc_post\<close> addsimprocs
-              [\<^simproc>\<open>NO_MATCH\<close>])
-            (Thm.rhs_of thm)
-        in @{thm Pure.transitive} OF [thm, post_simplified_ct] end)
+      let val post_simplified_ct =
+        Simplifier.full_rewrite (clear_simpset ctxt
+          addsimps Named_Theorems.get ctxt \<^named_theorems>\<open>cancelation_simproc_post\<close>
+          |> Simplifier.add_proc \<^simproc>\<open>NO_MATCH\<close>) (Thm.rhs_of thm)
+      in @{thm Pure.transitive} OF [thm, post_simplified_ct] end
   in
     Option.map (export o add_post_simplification o add_pre_simplification) canceled_thm
   end
diff -r 71910299bbcd -r cc4ecaa8e96e src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Tue Aug 13 21:09:51 2024 +0200
@@ -1380,8 +1380,10 @@
                                   simp_tac ind_ss1' i
                               | _ $ (Const (\<^const_name>\<open>Not\<close>, _) $ _) =>
                                   resolve_tac context2 freshs2' i
-                              | _ => asm_simp_tac (put_simpset HOL_basic_ss context3 addsimps
-                                  pt2_atoms addsimprocs [perm_simproc]) i)) 1])
+                              | _ =>
+                                asm_simp_tac (put_simpset HOL_basic_ss context3
+                                  addsimps pt2_atoms
+                                  |> Simplifier.add_proc perm_simproc) i)) 1])
                        val final = Proof_Context.export context3 context2 [th]
                      in
                        resolve_tac context2 final 1
@@ -1560,7 +1562,7 @@
                  resolve_tac ctxt [rec_induct] 1 THEN REPEAT
                  (simp_tac (put_simpset HOL_basic_ss ctxt
                     addsimps flat perm_simps'
-                    addsimprocs [NominalPermeq.perm_app_simproc]) 1 THEN
+                    |> Simplifier.add_proc NominalPermeq.perm_app_simproc) 1 THEN
                   (resolve_tac ctxt rec_intrs THEN_ALL_NEW
                    asm_simp_tac (put_simpset HOL_ss ctxt addsimps (fresh_bij @ perm_bij))) 1))))
         val ths' = map (fn ((P, Q), th) =>
@@ -1972,8 +1974,8 @@
                           (fn {context = ctxt, ...} => EVERY
                              [cut_facts_tac [th'] 1,
                               full_simp_tac (put_simpset HOL_ss ctxt
-                                addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap
-                                addsimprocs [NominalPermeq.perm_app_simproc]) 1,
+                                addsimps (rec_eqns @ pi1_pi2_eqs @ perm_swap)
+                                |> Simplifier.add_proc NominalPermeq.perm_app_simproc) 1,
                               full_simp_tac (put_simpset HOL_ss context'' addsimps (calc_atm @
                                 fresh_prems' @ freshs2' @ perm_fresh_fresh)) 1])
                       end;
@@ -2005,8 +2007,8 @@
                       (HOLogic.mk_Trueprop (HOLogic.mk_eq
                         (fold_rev (mk_perm []) pi1 rhs', fold_rev (mk_perm []) pi2 lhs')))
                       (fn _ => simp_tac (put_simpset HOL_ss context''
-                           addsimps pi1_pi2_eqs @ rec_eqns
-                           addsimprocs [NominalPermeq.perm_app_simproc]) 1 THEN
+                           addsimps (pi1_pi2_eqs @ rec_eqns)
+                           |> Simplifier.add_proc NominalPermeq.perm_app_simproc) 1 THEN
                          TRY (simp_tac (put_simpset HOL_ss context'' addsimps
                            (fresh_prems' @ freshs2' @ calc_atm @ perm_fresh_fresh)) 1));
 
diff -r 71910299bbcd -r cc4ecaa8e96e src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Aug 13 21:09:51 2024 +0200
@@ -280,8 +280,9 @@
     fun eqvt_ss ctxt =
       put_simpset HOL_basic_ss ctxt
         addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
-        addsimprocs [mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>],
-          NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc];
+        |> Simplifier.add_proc (mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>])
+        |> Simplifier.add_proc NominalPermeq.perm_app_simproc
+        |> Simplifier.add_proc NominalPermeq.perm_fun_simproc;
     val fresh_bij = Global_Theory.get_thms thy "fresh_bij";
     val perm_bij = Global_Theory.get_thms thy "perm_bij";
     val fs_atoms = map (fn aT => Global_Theory.get_thm thy
@@ -352,8 +353,9 @@
                     map (fold_rev (NominalDatatype.mk_perm [])
                       (rev pis' @ pis)) params' @ [z]))) ihyp;
                  fun mk_pi th =
-                   Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
-                       addsimprocs [NominalDatatype.perm_simproc])
+                   Simplifier.simplify (put_simpset HOL_basic_ss ctxt'
+                       addsimps [@{thm id_apply}]
+                       |> Simplifier.add_proc NominalDatatype.perm_simproc)
                      (Simplifier.simplify (eqvt_ss ctxt')
                        (fold_rev (mk_perm_bool ctxt' o Thm.cterm_of ctxt')
                          (rev pis' @ pis) th));
@@ -399,7 +401,7 @@
                      REPEAT_DETERM_N (length gprems)
                        (simp_tac (put_simpset HOL_basic_ss goal_ctxt4
                           addsimps [inductive_forall_def']
-                          addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
+                          |> Simplifier.add_proc NominalDatatype.perm_simproc) 1 THEN
                         resolve_tac goal_ctxt4 gprems2 1)]));
                  val final = Goal.prove ctxt' [] [] (Thm.term_of concl)
                    (fn {context = goal_ctxt5, ...} =>
@@ -468,8 +470,9 @@
 
     fun cases_eqvt_simpset ctxt =
       put_simpset HOL_ss ctxt
-        addsimps eqvt_thms @ swap_simps @ perm_pi_simp
-        addsimprocs [NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc];
+        addsimps (eqvt_thms @ swap_simps @ perm_pi_simp)
+        |> Simplifier.add_proc NominalPermeq.perm_app_simproc
+        |> Simplifier.add_proc NominalPermeq.perm_fun_simproc;
 
     fun simp_fresh_atm ctxt =
       Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps fresh_atm);
@@ -625,10 +628,12 @@
     val (([t], [pi]), ctxt1) = lthy |>
       Variable.import_terms false [Thm.concl_of raw_induct] ||>>
       Variable.variant_fixes ["pi"];
-    fun eqvt_simpset ctxt = put_simpset HOL_basic_ss ctxt addsimps
-      (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
-      [mk_perm_bool_simproc names,
-       NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc];
+    fun eqvt_simpset ctxt =
+      put_simpset HOL_basic_ss ctxt
+        addsimps (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp)
+        |> Simplifier.add_proc (mk_perm_bool_simproc names)
+        |> Simplifier.add_proc NominalPermeq.perm_app_simproc
+        |> Simplifier.add_proc NominalPermeq.perm_fun_simproc;
     val ps = map (fst o HOLogic.dest_imp)
       (HOLogic.dest_conj (HOLogic.dest_Trueprop t));
     fun eqvt_tac ctxt pi (intr, vs) st =
diff -r 71910299bbcd -r cc4ecaa8e96e src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Tue Aug 13 21:09:51 2024 +0200
@@ -299,8 +299,9 @@
     fun eqvt_ss ctxt =
       put_simpset HOL_basic_ss ctxt
         addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
-        addsimprocs [mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>],
-          NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc];
+        |> Simplifier.add_proc (mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>])
+        |> Simplifier.add_proc NominalPermeq.perm_app_simproc
+        |> Simplifier.add_proc NominalPermeq.perm_fun_simproc;
     val fresh_star_bij = Global_Theory.get_thms thy "fresh_star_bij";
     val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms;
     val at_insts = map (NominalAtoms.at_inst_of thy) atoms;
@@ -412,7 +413,7 @@
                  fun mk_pi th =
                    Simplifier.simplify
                      (put_simpset HOL_basic_ss ctxt'' addsimps [@{thm id_apply}]
-                       addsimprocs [NominalDatatype.perm_simproc])
+                       |> Simplifier.add_proc NominalDatatype.perm_simproc)
                      (Simplifier.simplify (eqvt_ss ctxt'')
                        (fold_rev (mk_perm_bool ctxt'' o Thm.cterm_of ctxt'')
                          (pis' @ pis) th));
@@ -435,7 +436,7 @@
                      [REPEAT_DETERM_N (length gprems)
                        (simp_tac (put_simpset HOL_basic_ss goal_ctxt4
                           addsimps [inductive_forall_def']
-                          addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
+                          |> Simplifier.add_proc NominalDatatype.perm_simproc) 1 THEN
                         resolve_tac goal_ctxt4 gprems2 1)]));
                  val final = Goal.prove ctxt'' [] [] (Thm.term_of concl)
                    (fn {context = goal_ctxt5, ...} =>
diff -r 71910299bbcd -r cc4ecaa8e96e src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Tue Aug 13 21:09:51 2024 +0200
@@ -142,7 +142,8 @@
     let
        val ctxt' = ctxt
          addsimps (maps (Proof_Context.get_thms ctxt) dyn_thms @ eqvt_thms)
-         addsimprocs [perm_fun_simproc, perm_app_simproc]
+         |> Simplifier.add_proc perm_fun_simproc
+         |> Simplifier.add_proc perm_app_simproc
          |> fold Simplifier.del_cong weak_congs
          |> fold Simplifier.add_cong strong_congs
     in
@@ -219,7 +220,7 @@
   ("analysing permutation compositions on the lhs",
    fn st => EVERY
      [resolve_tac ctxt [trans] i,
-      asm_full_simp_tac (empty_simpset ctxt addsimprocs [perm_compose_simproc]) i,
+      asm_full_simp_tac (empty_simpset ctxt |> Simplifier.add_proc perm_compose_simproc) i,
       asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [perm_aux_fold]) i] st);
 
 fun apply_cong_tac ctxt i = ("application of congruence", cong_tac ctxt i);
diff -r 71910299bbcd -r cc4ecaa8e96e src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Tue Aug 13 21:09:51 2024 +0200
@@ -80,18 +80,18 @@
   simp_tac (put_simpset HOL_basic_ss ctxt
     addsimps @{thms list.inject list.distinct char.inject
       cong_exp_iff_simps simp_thms}
-    addsimprocs [lazy_conj_simproc]
+    |> Simplifier.add_proc lazy_conj_simproc
     |> Simplifier.add_cong @{thm block_conj_cong});
 
 end;
 
 val lookup_ss =
-  simpset_of (put_simpset HOL_basic_ss \<^context>
+  simpset_of ((put_simpset HOL_basic_ss \<^context>
     addsimps (@{thms list.inject} @ @{thms char.inject}
       @ @{thms list.distinct} @ @{thms simp_thms}
       @ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel},
         @{thm StateFun.lookup_update_same}, @{thm StateFun.lookup_update_other}])
-    addsimprocs [lazy_conj_simproc]
+    |> Simplifier.add_proc lazy_conj_simproc)
     addSolver StateSpace.distinctNameSolver
     |> fold Simplifier.add_cong @{thms block_conj_cong});
 
@@ -173,7 +173,8 @@
   simpset_of (put_simpset HOL_ss \<^context> addsimps
     (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms char.inject}
       @ @{thms list.distinct})
-    addsimprocs [lazy_conj_simproc, StateSpace.distinct_simproc]
+    |> Simplifier.add_proc lazy_conj_simproc
+    |> Simplifier.add_proc StateSpace.distinct_simproc
     |> fold Simplifier.add_cong @{thms block_conj_cong});
 
 in
@@ -395,7 +396,7 @@
                 (simpset_map ctxt (Simplifier.add_simp thm) lookup_ss, ex_lookup_ss));
           val activate_simprocs =
             if simprocs_active then I
-            else Simplifier.map_ss (fn ctxt => ctxt addsimprocs [lookup_simproc, update_simproc]);
+            else Simplifier.map_ss (fold Simplifier.add_proc [lookup_simproc, update_simproc]);
         in
           context
           |> activate_simprocs
diff -r 71910299bbcd -r cc4ecaa8e96e src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Statespace/state_space.ML	Tue Aug 13 21:09:51 2024 +0200
@@ -338,7 +338,7 @@
           val tt' = tt |> fold upd all_names;
           val context' =
               Context_Position.set_visible false ctxt
-              addsimprocs [distinct_simproc]
+              |> Simplifier.add_proc distinct_simproc
               |> Context_Position.restore_visible ctxt
               |> Context.Proof
               |> map_declinfo (K declinfo)
diff -r 71910299bbcd -r cc4ecaa8e96e src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Tools/record.ML	Tue Aug 13 21:09:51 2024 +0200
@@ -1442,11 +1442,11 @@
               else NONE
             end));
 
-    val simprocs = if has_rec goal then [split_simproc P] else [];
+    val add_simproc = if has_rec goal then Simplifier.add_proc (split_simproc P) else I;
     val thms' = @{thms o_apply K_record_comp} @ thms;
   in
     EVERY split_frees_tacs THEN
-    full_simp_tac (put_simpset (get_simpset thy) ctxt addsimps thms' addsimprocs simprocs) i
+    full_simp_tac (put_simpset (get_simpset thy) ctxt addsimps thms' |> add_simproc) i
   end);
 
 
diff -r 71910299bbcd -r cc4ecaa8e96e src/Tools/induct.ML
--- a/src/Tools/induct.ML	Tue Aug 13 19:28:58 2024 +0200
+++ b/src/Tools/induct.ML	Tue Aug 13 21:09:51 2024 +0200
@@ -229,8 +229,8 @@
     ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
      (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
      (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)),
-     simpset_of (empty_simpset \<^context>
-      addsimprocs [rearrange_eqs_simproc] addsimps [Drule.norm_hhf_eq]));
+     simpset_of ((empty_simpset \<^context>
+      |> Simplifier.add_proc rearrange_eqs_simproc) addsimps [Drule.norm_hhf_eq]));
   fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1), simpset1),
       ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2), simpset2)) =
     ((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)),