clarified signature;
authorwenzelm
Wed, 20 Dec 2023 12:50:16 +0100
changeset 79317 788921b906e1
parent 79316 7464bb64622d
child 79318 74e245625a67
clarified signature;
src/Pure/term_items.ML
--- a/src/Pure/term_items.ML	Wed Dec 20 11:55:04 2023 +0100
+++ b/src/Pure/term_items.ML	Wed Dec 20 12:50:16 2023 +0100
@@ -10,6 +10,7 @@
 sig
   structure Key: KEY
   type key
+  exception DUP of key
   type 'a table
   val empty: 'a table
   val build: ('a table -> 'a table) -> 'a table
@@ -32,7 +33,7 @@
   val make1: key * 'a -> 'a table
   val make2: key * 'a -> key * 'a -> 'a table
   val make3: key * 'a -> key * 'a -> key * 'a -> 'a table
-  val make_strict: (key * 'a) list -> 'a table
+  val make_strict: (key * 'a) list -> 'a table  (*exception DUP*)
   val unsynchronized_cache: (key -> 'a) -> key -> 'a
   type set = int table
   val add_set: key -> set -> set
@@ -58,6 +59,7 @@
 (* table with length *)
 
 structure Table = Table(Key);
+exception DUP = Table.DUP;
 
 datatype 'a table = Table of 'a Table.table;