# HG changeset patch
# User wenzelm
# Date 1680085524 -7200
# Node ID 33bee7a96f721c12867703307150daf7bd49dc93
# Parent  676713cba24dbdfc58c34c5cf269862e225af612
tuned comments (amending 1951f6470792);

diff -r 676713cba24d -r 33bee7a96f72 src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Wed Mar 29 12:24:50 2023 +0200
+++ b/src/Pure/General/set.ML	Wed Mar 29 12:25:24 2023 +0200
@@ -95,7 +95,7 @@
 end;
 
 
-(* empty and single *)
+(* empty *)
 
 val empty = Empty;
 
diff -r 676713cba24d -r 33bee7a96f72 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Wed Mar 29 12:24:50 2023 +0200
+++ b/src/Pure/General/table.ML	Wed Mar 29 12:25:24 2023 +0200
@@ -115,7 +115,7 @@
   | unmake arg = arg;
 
 
-(* empty and single *)
+(* empty *)
 
 val empty = Empty;