# HG changeset patch
# User wenzelm
# Date 1723654789 -7200
# Node ID 3f2c371a3de9a38f63e5e66623a5e4dbfa1406ae
# Parent  897c993293c58068ef8f40354b9d29f3ddccc83f
tuned;

diff -r 897c993293c5 -r 3f2c371a3de9 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Aug 14 16:48:16 2024 +0200
+++ b/src/Pure/simplifier.ML	Wed Aug 14 18:59:49 2024 +0200
@@ -281,18 +281,17 @@
     fun pretty_cong (name, thm) =
       Pretty.block [pretty_cong_name name, Pretty.str ":", Pretty.brk 1, pretty_thm thm];
 
-    val {simps, simprocs, congs, loopers, unsafe_solvers, safe_solvers, ...} =
-      dest_ss (simpset_of ctxt);
+    val ss = dest_ss (simpset_of ctxt);
     val simprocs =
       Name_Space.markup_entries verbose ctxt
-        (Name_Space.space_of_table (get_simprocs ctxt)) simprocs;
+        (Name_Space.space_of_table (get_simprocs ctxt)) (#simprocs ss);
   in
-    [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps),
+    [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) (#simps ss)),
       Pretty.big_list "simplification procedures:" (map pretty_simproc simprocs),
-      Pretty.big_list "congruences:" (map pretty_cong congs),
-      Pretty.strs ("loopers:" :: map quote loopers),
-      Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers),
-      Pretty.strs ("safe solvers:" :: map quote safe_solvers)]
+      Pretty.big_list "congruences:" (map pretty_cong (#congs ss)),
+      Pretty.strs ("loopers:" :: map quote (#loopers ss)),
+      Pretty.strs ("unsafe solvers:" :: map quote (#unsafe_solvers ss)),
+      Pretty.strs ("safe solvers:" :: map quote (#safe_solvers ss))]
     |> Pretty.chunks
   end;