diff -r 62616d8422c5 -r aca84704d46f src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Oct 20 22:19:05 2023 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat Oct 21 00:13:12 2023 +0200
@@ -298,7 +298,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_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;