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, ...} =>