--- a/src/HOL/HOL.thy Tue Aug 13 18:31:40 2024 +0200
+++ b/src/HOL/HOL.thy Tue Aug 13 18:53:24 2024 +0200
@@ -1567,11 +1567,12 @@
| _ => NONE)\<close>
declaration \<open>
- K (Induct.map_simpset (fn ss => ss
- addsimprocs [\<^simproc>\<open>swap_induct_false\<close>, \<^simproc>\<open>induct_equal_conj_curry\<close>]
- |> Simplifier.set_mksimps (fn ctxt =>
- Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
- map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))))
+ K (Induct.map_simpset
+ (Simplifier.add_proc \<^simproc>\<open>swap_induct_false\<close> #>
+ Simplifier.add_proc \<^simproc>\<open>induct_equal_conj_curry\<close> #>
+ Simplifier.set_mksimps (fn ctxt =>
+ Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
+ map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback})))))
\<close>
text \<open>Pre-simplification of induction and cases rules\<close>
@@ -1942,7 +1943,7 @@
\<^Const_>\<open>HOL.eq T\<close> => if is_Type T then SOME @{thm eq_equal} else NONE
| _ => NONE)\<close>
-setup \<open>Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs [\<^simproc>\<open>equal\<close>])\<close>
+setup \<open>Code_Preproc.map_pre (Simplifier.add_proc \<^simproc>\<open>equal\<close>)\<close>
subsubsection \<open>Generic code generator foundation\<close>