--- a/src/Pure/General/set.ML	Sun Apr 02 12:34:13 2023 +0200
+++ b/src/Pure/General/set.ML	Mon Apr 03 21:13:46 2023 +0200
@@ -81,6 +81,7 @@
 
 (* size *)
 
+(*literal copy from table.ML*)
 local
   fun count Empty n = n
     | count (Leaf1 _) n = n + 1
changeset 77780	97febdb6ee58
parent 77768	65008644d394
child 77800	9a30b76a6f60