src/Pure/General/table.ML

--- a/src/Pure/General/table.ML	Tue Mar 28 19:03:39 2023 +0200
+++ b/src/Pure/General/table.ML	Tue Mar 28 19:07:58 2023 +0200
@@ -67,9 +67,13 @@
 functor Table(Key: KEY): TABLE =
 struct
 
+(* keys *)
+
 structure Key = Key;
 type key = Key.key;
 
+exception DUP of key;
+
 
 (* datatype *)
 
@@ -78,8 +82,6 @@
   Branch2 of 'a table * (key * 'a) * 'a table |
   Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;
 
-exception DUP of key;
-
 
 (* empty and single *)