src/Pure/General/table.ML

 
 
 (* size *)
 
 (*literal copy from set.ML*)
-fun make_size m arg = if m > 12 then Size (m, arg) else arg;
-
 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)))
     | count (Size (m, _)) n = m + n;
+
+  fun box (Branch2 _) = 1
+    | box (Branch3 _) = 1
+    | box _ = 0;
+
+  fun bound arg b =
+    if b > 0 then
+      (case arg of
+        Branch2 (left, _, right) =>
+          bound right (bound left (b - box left - box right))
+      | Branch3 (left, _, mid, _, right) =>
+          bound right (bound mid (bound left (b - box left - box mid - box right)))
+      | _ => b)
+    else b;
 in
-  fun size tab = Integer.build (count tab);
+  fun size arg = count arg 0;
+  fun make_size m arg = if bound arg 3 <= 0 then Size (m, arg) else arg;
 end;
 
 
 (* empty *)