--- a/src/HOL/Tools/SMT/smt_replay_methods.ML Thu Aug 07 13:06:42 2025 +0200
+++ b/src/HOL/Tools/SMT/smt_replay_methods.ML Thu Aug 07 13:18:15 2025 +0200
@@ -399,12 +399,13 @@
Method.insert_tac ctxt prems
THEN' SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms z3div_def z3mod_def int_distrib})
THEN' Simplifier.asm_full_simp_tac
- (empty_simpset ctxt addsimprocs [(*@{simproc linordered_ring_strict_eq_cancel_factor_poly},
- @{simproc linordered_ring_strict_le_cancel_factor_poly},
- @{simproc linordered_ring_strict_less_cancel_factor_poly},
- @{simproc nat_eq_cancel_factor_poly},
- @{simproc nat_le_cancel_factor_poly},
- @{simproc nat_less_cancel_factor_poly}*)])
+ (empty_simpset ctxt |> fold Simplifier.add_proc
+ [(*@{simproc linordered_ring_strict_eq_cancel_factor_poly},
+ @{simproc linordered_ring_strict_le_cancel_factor_poly},
+ @{simproc linordered_ring_strict_less_cancel_factor_poly},
+ @{simproc nat_eq_cancel_factor_poly},
+ @{simproc nat_le_cancel_factor_poly},
+ @{simproc nat_less_cancel_factor_poly}*)])
THEN' (fn i => TRY (Arith_Data.arith_tac ctxt i))
fun arith_th_lemma_wo ctxt thms t =
--- a/src/HOL/Tools/record.ML Thu Aug 07 13:06:42 2025 +0200
+++ b/src/HOL/Tools/record.ML Thu Aug 07 13:18:15 2025 +0200
@@ -1029,8 +1029,11 @@
in
Goal.prove ctxt [] [] prop'
(fn {context = ctxt', ...} =>
- simp_tac (put_simpset HOL_basic_ss ctxt' addsimps (simps @ @{thms K_record_comp})) 1 THEN
- TRY (simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ex_simps addsimprocs ex_simprs) 1))
+ let val ctxt0 = put_simpset HOL_basic_ss ctxt' in
+ simp_tac (ctxt0 |> Simplifier.add_simps (simps @ @{thms K_record_comp})) 1 THEN
+ TRY (simp_tac
+ (ctxt0 |> Simplifier.add_simps ex_simps |> fold Simplifier.add_proc ex_simprs) 1)
+ end)
end;
--- a/src/HOL/ex/Simproc_Tests.thy Thu Aug 07 13:06:42 2025 +0200
+++ b/src/HOL/ex/Simproc_Tests.thy Thu Aug 07 13:18:15 2025 +0200
@@ -17,8 +17,8 @@
subsection \<open>ML bindings\<close>
ML \<open>
- fun test ctxt ps =
- CHANGED (asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimprocs ps) 1)
+ fun test ctxt procs =
+ CHANGED (asm_simp_tac (put_simpset HOL_basic_ss ctxt |> fold Simplifier.add_proc procs) 1)
\<close>
subsection \<open>Cancellation simprocs from \<open>Nat.thy\<close>\<close>
@@ -398,8 +398,8 @@
assume z_pos: "0 < z"
assume "x < y" have "z*x < z*y"
by (tactic \<open>CHANGED (asm_simp_tac (put_simpset HOL_basic_ss \<^context>
- addsimprocs [\<^simproc>\<open>linordered_ring_less_cancel_factor\<close>]
- addsimps [@{thm z_pos}]) 1)\<close>) fact
+ |> Simplifier.add_proc \<^simproc>\<open>linordered_ring_less_cancel_factor\<close>
+ |> Simplifier.add_simp @{thm z_pos}) 1)\<close>) fact
}
end
--- a/src/Provers/Arith/fast_lin_arith.ML Thu Aug 07 13:06:42 2025 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Thu Aug 07 13:18:15 2025 +0200
@@ -166,8 +166,8 @@
fun add_inj_thms thms = map_data (map_inj_thms (append (map Thm.trim_context thms)));
fun add_lessD thm = map_data (map_lessD (fn thms => thms @ [Thm.trim_context thm]));
-fun add_simps thms = map_simpset (fn ctxt => ctxt addsimps thms);
-fun add_simprocs procs = map_simpset (fn ctxt => ctxt addsimprocs procs);
+val add_simps = map_simpset o Simplifier.add_simps;
+val add_simprocs = map_simpset o fold Simplifier.add_proc;
fun set_number_of f =
map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, ...} =>