--- 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 *)
--- 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);
--- 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);
--- 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 |
--- 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);