# HG changeset patch
# User wenzelm
# Date 1680018681 -7200
# Node ID 0ad86d5b3bc356415e15d65a30dee79b9a01a4d2
# Parent  b0d3951232ad9990aaa6fd2a0f0243f2225b0cc7
tuned;

diff -r b0d3951232ad -r 0ad86d5b3bc3 src/Pure/term_ord.ML
--- 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);