tuned;

--- a/src/Pure/more_thm.ML	Wed Sep 08 08:41:36 2021 +0200
+++ b/src/Pure/more_thm.ML	Thu Sep 09 10:40:57 2021 +0200
@@ -218,7 +218,7 @@
   ||| list_ord Term_Ord.sort_ord o apply2 Thm.shyps_of;
 
 
-(* tables and caches *)
+(* scalable collections *)
 
 structure Ctermtab = Table(type key = cterm val ord = fast_term_ord);
 structure Thmtab = Table(type key = thm val ord = thm_ord);

--- a/src/Pure/term_ord.ML	Wed Sep 08 08:41:36 2021 +0200
+++ b/src/Pure/term_ord.ML	Thu Sep 09 10:40:57 2021 +0200
@@ -1,7 +1,8 @@
 (*  Title:      Pure/term_ord.ML
-    Author:     Tobias Nipkow and Makarius, TU Muenchen
+    Author:     Tobias Nipkow, TU Muenchen
+    Author:     Makarius
 
-Term orderings.
+Term orderings and scalable collections.
 *)
 
 signature BASIC_TERM_ORD =
@@ -10,6 +11,10 @@
   structure Sorttab: TABLE
   structure Typtab: TABLE
   structure Termtab: TABLE
+  structure Var_Graph: GRAPH
+  structure Sort_Graph: GRAPH
+  structure Typ_Graph: GRAPH
+  structure Term_Graph: GRAPH
 end;
 
 signature TERM_ORD =
@@ -209,22 +214,21 @@
 end;
 
 
-(* tables and caches *)
+(* scalable collections *)
 
 structure Vartab = Table(type key = indexname val ord = fast_indexname_ord);
 structure Sorttab = Table(type key = sort val ord = sort_ord);
 structure Typtab = Table(type key = typ val ord = typ_ord);
 structure Termtab = Table(type key = term val ord = fast_term_ord);
 
+structure Var_Graph = Graph(type key = indexname val ord = fast_indexname_ord);
+structure Sort_Graph = Graph(type key = sort val ord = sort_ord);
+structure Typ_Graph = Graph(type key = typ val ord = typ_ord);
+structure Term_Graph = Graph(type key = term val ord = fast_term_ord);
+
 fun term_cache f = Cache.create Termtab.empty Termtab.lookup Termtab.update f;
 
 end;
 
 structure Basic_Term_Ord: BASIC_TERM_ORD = Term_Ord;
 open Basic_Term_Ord;
-
-structure Var_Graph = Graph(type key = indexname val ord = Term_Ord.fast_indexname_ord);
-structure Sort_Graph = Graph(type key = sort val ord = Term_Ord.sort_ord);
-structure Typ_Graph = Graph(type key = typ val ord = Term_Ord.typ_ord);
-structure Term_Graph = Graph(type key = term val ord = Term_Ord.fast_term_ord);
-