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 =