# HG changeset patch
# User wenzelm
# Date 1680019845 -7200
# Node ID 48fbecc8fab13f397910291e3fe9c1a40ddb1c90
# Parent  4a174bea55e2b2fbbbb13a91fee0e8c1ad4ef012
tuned signature: more uniform structure Key;

diff -r 4a174bea55e2 -r 48fbecc8fab1 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Tue Mar 28 17:59:54 2023 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Tue Mar 28 18:10:45 2023 +0200
@@ -182,7 +182,7 @@
 end;
 
 structure Tasks = Set(type key = task val ord = task_ord);
-structure Task_Graph = Graph(type key = task val ord = task_ord);
+structure Task_Graph = Graph(Tasks.Key);
 
 
 (* timing *)
diff -r 4a174bea55e2 -r 48fbecc8fab1 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Tue Mar 28 17:59:54 2023 +0200
+++ b/src/Pure/General/graph.ML	Tue Mar 28 18:10:45 2023 +0200
@@ -6,6 +6,7 @@
 
 signature GRAPH =
 sig
+  structure Key: KEY
   type key
   structure Keys:
   sig
@@ -72,7 +73,9 @@
 
 (* keys *)
 
+structure Key = Key;
 type key = Key.key;
+
 val eq_key = is_equal o Key.ord;
 
 structure Table = Table(Key);
@@ -352,6 +355,6 @@
 
 end;
 
-structure Graph = Graph(type key = string val ord = fast_string_ord);
+structure Graph = Graph(Symtab.Key);
 structure String_Graph = Graph(type key = string val ord = string_ord);
-structure Int_Graph = Graph(type key = int val ord = int_ord);
+structure Int_Graph = Graph(Inttab.Key);
diff -r 4a174bea55e2 -r 48fbecc8fab1 src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Tue Mar 28 17:59:54 2023 +0200
+++ b/src/Pure/General/set.ML	Tue Mar 28 18:10:45 2023 +0200
@@ -6,6 +6,7 @@
 
 signature SET =
 sig
+  structure Key: KEY
   type elem
   type T
   val size: T -> int
@@ -32,9 +33,11 @@
 functor Set(Key: KEY): SET =
 struct
 
-(* datatype *)
+structure Key = Key;
+type elem = Key.key;
 
-type elem = Key.key;
+
+(* datatype *)
 
 datatype T =
   Empty |
@@ -339,5 +342,5 @@
 
 end;
 
-structure Intset = Set(type key = int val ord = int_ord);
-structure Symset = Set(type key = string val ord = fast_string_ord);
+structure Intset = Set(Inttab.Key);
+structure Symset = Set(Symtab.Key);
diff -r 4a174bea55e2 -r 48fbecc8fab1 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Tue Mar 28 17:59:54 2023 +0200
+++ b/src/Pure/General/table.ML	Tue Mar 28 18:10:45 2023 +0200
@@ -13,6 +13,7 @@
 
 signature TABLE =
 sig
+  structure Key: KEY
   type key
   type 'a table
   exception DUP of key
@@ -66,10 +67,11 @@
 functor Table(Key: KEY): TABLE =
 struct
 
+structure Key = Key;
+type key = Key.key;
 
-(* datatype table *)
 
-type key = Key.key;
+(* datatype *)
 
 datatype 'a table =
   Empty |
diff -r 4a174bea55e2 -r 48fbecc8fab1 src/Pure/term_ord.ML
--- a/src/Pure/term_ord.ML	Tue Mar 28 17:59:54 2023 +0200
+++ b/src/Pure/term_ord.ML	Tue Mar 28 18:10:45 2023 +0200
@@ -222,7 +222,7 @@
 
 end;
 
-structure Termset = Set(type key = term val ord = Term_Ord.fast_term_ord);
+structure Termset = Set(Termtab.Key);
 
 structure Sortset:
 sig
@@ -234,7 +234,7 @@
 end =
 struct
 
-structure Set = Set(type key = sort val ord = Term_Ord.sort_ord);
+structure Set = Set(Sorttab.Key);
 open Set;
 
 fun insert_typ (TFree (_, S)) Ss = insert S Ss
@@ -255,7 +255,7 @@
 
 end;
 
-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);
+structure Var_Graph = Graph(Vartab.Key);
+structure Sort_Graph = Graph(Sorttab.Key);
+structure Typ_Graph = Graph(Typtab.Key);
+structure Term_Graph = Graph(Termtab.Key);