--- a/src/Tools/induct.ML Tue Aug 13 19:28:58 2024 +0200
+++ b/src/Tools/induct.ML Tue Aug 13 21:09:51 2024 +0200
@@ -229,8 +229,8 @@
((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
(init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
(init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)),
- simpset_of (empty_simpset \<^context>
- addsimprocs [rearrange_eqs_simproc] addsimps [Drule.norm_hhf_eq]));
+ simpset_of ((empty_simpset \<^context>
+ |> Simplifier.add_proc rearrange_eqs_simproc) addsimps [Drule.norm_hhf_eq]));
fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1), simpset1),
((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2), simpset2)) =
((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)),