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