# HG changeset patch
# User wenzelm
# Date 1635278673 -7200
# Node ID 71bafd70acbb43627511b0e4d9876934f3cc2802
# Parent  2f28a0a758abc58514c47605d3a1654c8ca9873b
avoid waste of resources due to dynamic simpset (amending 45c09620f726);

diff -r 2f28a0a758ab -r 71bafd70acbb src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Tue Oct 26 17:14:16 2021 +0200
+++ b/src/HOL/Tools/record.ML	Tue Oct 26 22:04:33 2021 +0200
@@ -2117,16 +2117,17 @@
     (* 3rd stage: thms_thy *)
 
     val record_ss = get_simpset defs_thy;
-    fun sel_upd_ctxt ctxt' =
-      put_simpset record_ss ctxt'
-        addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms);
+    val sel_upd_ss =
+      simpset_of
+        (put_simpset record_ss defs_ctxt
+          addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms));
 
     val (sel_convs, upd_convs) =
       timeit_msg defs_ctxt "record sel_convs/upd_convs proof:" (fn () =>
         grouped 10 Par_List.map (fn prop =>
             Goal.prove_sorry_global defs_thy [] [] prop
               (fn {context = ctxt', ...} =>
-                ALLGOALS (asm_full_simp_tac (sel_upd_ctxt ctxt'))))
+                ALLGOALS (asm_full_simp_tac (put_simpset sel_upd_ss ctxt'))))
           (sel_conv_props @ upd_conv_props))
       |> chop (length sel_conv_props);