# HG changeset patch
# User wenzelm
# Date 1680023278 -7200
# Node ID 59c94a376a3c2eb3865e5feaf595914825016260
# Parent  7d014af4007297e19ea67b5df08a2aba4fb07205
tuned;

diff -r 7d014af40072 -r 59c94a376a3c src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Tue Mar 28 19:03:39 2023 +0200
+++ b/src/Pure/General/set.ML	Tue Mar 28 19:07:58 2023 +0200
@@ -33,6 +33,8 @@
 functor Set(Key: KEY): SET =
 struct
 
+(* keys *)
+
 structure Key = Key;
 type elem = Key.key;
 
diff -r 7d014af40072 -r 59c94a376a3c 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 *)