diff -r 622ba814e01c -r 53c5ad1a7ac0 src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Tue Apr 11 09:01:09 2023 +0200
+++ b/src/Pure/General/set.ML	Tue Apr 11 09:49:30 2023 +0200
@@ -49,7 +49,6 @@
   Branch3 of T * elem * T * elem * T |
   Size of int * T;
 
-(*literal copy from table.ML*)
 fun make2 (Empty, e, Empty) = Leaf1 e
   | make2 (Branch2 (Empty, e1, Empty), e2, right) = make2 (Leaf1 e1, e2, right)
   | make2 (left, e1, Branch2 (Empty, e2, Empty)) = make2 (left, e1, Leaf1 e2)
@@ -62,7 +61,6 @@
   | make2 (Empty, e1, Leaf2 (e2, e3)) = Leaf3 (e1, e2, e3)
   | make2 arg = Branch2 arg;
 
-(*literal copy from table.ML*)
 fun make3 (Empty, e1, Empty, e2, Empty) = Leaf2 (e1, e2)
   | make3 (Branch2 (Empty, e1, Empty), e2, mid, e3, right) = make3 (Leaf1 e1, e2, mid, e3, right)
   | make3 (left, e1, Branch2 (Empty, e2, Empty), e3, right) = make3 (left, e1, Leaf1 e2, e3, right)
@@ -72,7 +70,6 @@
   | make3 (Empty, e1, Empty, e2, Leaf1 e3) = Leaf3 (e1, e2, e3)
   | make3 arg = Branch3 arg;
 
-(*literal copy from table.ML*)
 fun unmake (Leaf1 e) = Branch2 (Empty, e, Empty)
   | unmake (Leaf2 (e1, e2)) = Branch3 (Empty, e1, Empty, e2, Empty)
   | unmake (Leaf3 (e1, e2, e3)) =
@@ -341,7 +338,6 @@
 
 exception UNDEF of elem;
 
-(*literal copy from table.ML*)
 fun del (SOME k) Empty = raise UNDEF k
   | del NONE Empty = raise Match
   | del NONE (Leaf1 p) = (p, (true, Empty))