--- a/src/HOL/Tools/numeral_simprocs.ML Tue Aug 13 18:31:40 2024 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Tue Aug 13 18:53:24 2024 +0200
@@ -719,8 +719,8 @@
inverse_divide
divide_inverse_commute [symmetric]
simp_thms}
- addsimprocs field_cancel_numeral_factors
- addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc]
+ |> fold Simplifier.add_proc field_cancel_numeral_factors
+ |> fold Simplifier.add_proc [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc]
|> Simplifier.add_cong @{thm if_weak_cong})
in