tuned;

--- a/src/Pure/term_ord.ML	Tue Mar 28 17:32:09 2023 +0200
+++ b/src/Pure/term_ord.ML	Tue Mar 28 17:51:21 2023 +0200
@@ -210,17 +210,21 @@
 
 structure Termtab:
 sig
-  include TABLE;
+  include TABLE
   val term_cache: (term -> 'a) -> term -> 'a
 end =
 struct
-  structure Table = Table(type key = term val ord = Term_Ord.fast_term_ord);
-  open Table;
-  fun term_cache f = Cache.create empty lookup update f;
+
+structure Table = Table(type key = term val ord = Term_Ord.fast_term_ord);
+open Table;
+
+fun term_cache f = Cache.create empty lookup update f;
+
 end;
 
+structure Termset = Set(type key = term val ord = Term_Ord.fast_term_ord);
+
 structure Sortset = Set(type key = sort val ord = Term_Ord.sort_ord);
-structure Termset = Set(type key = term val ord = Term_Ord.fast_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);