# HG changeset patch
# User wenzelm
# Date 1680549226 -7200
# Node ID 97febdb6ee5856d804b128a68b2eee277317a1c1
# Parent  1f990c8bb74cb10686f8bd96ec46e4303f9a5480
clarified signature: more uniform Table() vs. Set();

diff -r 1f990c8bb74c -r 97febdb6ee58 src/Pure/General/set.ML
--- 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
diff -r 1f990c8bb74c -r 97febdb6ee58 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sun Apr 02 12:34:13 2023 +0200
+++ b/src/Pure/General/table.ML	Mon Apr 03 21:13:46 2023 +0200
@@ -19,6 +19,7 @@
   exception DUP of key
   exception SAME
   exception UNDEF of key
+  val size: 'a table -> int
   val empty: 'a table
   val build: ('a table -> 'a table) -> 'a table
   val is_empty: 'a table -> bool
@@ -115,6 +116,21 @@
   | unmake arg = arg;
 
 
+(* size *)
+
+local
+  (*literal copy from set.ML*)
+  fun count Empty n = n
+    | count (Leaf1 _) n = n + 1
+    | count (Leaf2 _) n = n + 2
+    | count (Leaf3 _) n = n + 3
+    | count (Branch2 (left, _, right)) n = count right (count left (n + 1))
+    | count (Branch3 (left, _, mid, _, right)) n = count right (count mid (count left (n + 2)));
+in
+  fun size tab = Integer.build (count tab);
+end;
+
+
 (* empty *)
 
 val empty = Empty;