--- 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;