# HG changeset patch
# User wenzelm
# Date 1684586886 -7200
# Node ID 3357bc875b11f7957829964885455d49098570de
# Parent  a51d2e96203e78b9bd14f550583ce585c89b3683
prefer static simpset;

diff -r a51d2e96203e -r 3357bc875b11 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sat May 20 14:12:01 2023 +0200
+++ b/src/HOL/Parity.thy	Sat May 20 14:48:06 2023 +0200
@@ -1323,11 +1323,10 @@
       minus_minus numeral_times_numeral mult_zero_right mult_1_right
       euclidean_size_nat_less_eq_iff euclidean_size_int_less_eq_iff diff_nat_numeral nat_numeral}
       @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}];
-    fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
-      (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps)
-  in
-    K (fn ctxt => successful_rewrite (Simplifier.put_simpset (prepare_simpset ctxt) ctxt))
-  end
+    val simpset =
+      HOL_ss |> Simplifier.simpset_map \<^context>
+        (Simplifier.add_cong if_cong #> fold Simplifier.add_simp simps);
+  in K (fn ctxt => successful_rewrite (Simplifier.put_simpset simpset ctxt)) end
 \<close> \<comment> \<open>
   There is space for improvement here: the calculation itself
   could be carried out outside the logic, and a generic simproc