# HG changeset patch
# User wenzelm
# Date 1703073016 -3600
# Node ID 788921b906e1aebd241f0df22cb5dd360c25dbd1
# Parent  7464bb64622da143e9e7b31b6cbfa785b46537e0
clarified signature;

diff -r 7464bb64622d -r 788921b906e1 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;