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