# HG changeset patch
# User wenzelm
# Date 1701371494 -3600
# Node ID 48187f1a615e0f91e2f046ae4d20dab952b53ebd
# Parent  3bdd3cf5f5e03c7d496112b6f60572190bce7a49
reduce redundancy: avoid huge lists;

diff -r 3bdd3cf5f5e0 -r 48187f1a615e src/Pure/term_ord.ML
--- a/src/Pure/term_ord.ML	Thu Nov 30 16:33:00 2023 +0100
+++ b/src/Pure/term_ord.ML	Thu Nov 30 20:11:34 2023 +0100
@@ -238,6 +238,7 @@
 
 end;
 
+structure Typset = Set(Typtab.Key);
 structure Termset = Set(Termtab.Key);
 
 structure Var_Graph = Graph(Vartab.Key);
diff -r 3bdd3cf5f5e0 -r 48187f1a615e src/Tools/profiling.ML
--- a/src/Tools/profiling.ML	Thu Nov 30 16:33:00 2023 +0100
+++ b/src/Tools/profiling.ML	Thu Nov 30 20:11:34 2023 +0100
@@ -64,8 +64,9 @@
     val thms = maps all_thms thys;
     val thys_id = map Context.theory_id thys;
     val thms_id = map Thm.theory_id thms;
-    val terms = (fold o Thm.fold_terms {hyps = true}) cons thms [];
-    val types = (fold o fold_types) cons terms [];
+    val terms =
+      Termset.dest ((fold o Thm.fold_terms {hyps = true}) Termset.insert thms Termset.empty);
+    val types = Typset.dest ((fold o fold_types) Typset.insert terms Typset.empty);
     val spaces =
       maps (fn f => map f thys)
        [Sign.class_space,
@@ -77,7 +78,7 @@
         Locale.locale_space,
         Attrib.attribute_space o Context.Theory,
         Method.method_space o Context.Theory];
-     val names = maps Name_Space.get_names spaces;
+     val names = Symset.dest (Symset.merges (map (Symset.make o Name_Space.get_names) spaces));
   in
     {thys_id = thys_id, thms_id = thms_id, terms = terms,
       types = types, names = names, spaces = spaces}