diff -r 62616d8422c5 -r aca84704d46f src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Fri Oct 20 22:19:05 2023 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Sat Oct 21 00:13:12 2023 +0200
@@ -279,7 +279,7 @@
       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_simproc_app, NominalPermeq.perm_simproc_fun];
+          NominalPermeq.perm_app_simproc, 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
@@ -467,7 +467,7 @@
     fun cases_eqvt_simpset ctxt =
       put_simpset HOL_ss ctxt
         addsimps eqvt_thms @ swap_simps @ perm_pi_simp
-        addsimprocs [NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
+        addsimprocs [NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc];
 
     fun simp_fresh_atm ctxt =
       Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps fresh_atm);
@@ -626,7 +626,7 @@
     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_simproc_app, NominalPermeq.perm_simproc_fun];
+       NominalPermeq.perm_app_simproc, 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 =