# HG changeset patch
# User wenzelm
# Date 1680036185 -7200
# Node ID 570f1436fe0aaa0893cfd98645c8280e7991d707
# Parent  be3f838b3e17b0c94df4b0266363ea23d93bde3c
more compact representation of leaf nodes: only 1.10 .. 1.33 larger than plain list;

diff -r be3f838b3e17 -r 570f1436fe0a src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Tue Mar 28 19:43:49 2023 +0200
+++ b/src/Pure/General/set.ML	Tue Mar 28 22:43:05 2023 +0200
@@ -38,19 +38,34 @@
 structure Key = Key;
 type elem = Key.key;
 
+val eq_key = is_equal o Key.ord;
 
 (* datatype *)
 
 datatype T =
   Empty |
+  Leaf1 of elem |
+  Leaf2 of elem * elem |
   Branch2 of T * elem * T |
   Branch3 of T * elem * T * elem * T;
 
+fun make2 (Empty, e, Empty) = Leaf1 e
+  | make2 arg = Branch2 arg;
+
+fun make3 (Empty, e1, Empty, e2, Empty) = Leaf2 (e1, e2)
+  | make3 arg = Branch3 arg;
+
+fun unmake (Leaf1 e) = Branch2 (Empty, e, Empty)
+  | unmake (Leaf2 (e1, e2)) = Branch3 (Empty, e1, Empty, e2, Empty)
+  | unmake arg = arg;
+
 
 (* size *)
 
 local
   fun add_size Empty n = n
+    | add_size (Leaf1 _) n = n + 1
+    | add_size (Leaf2 _) n = n + 2
     | add_size (Branch2 (left, _, right)) n =
         n + 1 |> add_size left |> add_size right
     | add_size (Branch3 (left, _, mid, _, right)) n =
@@ -69,7 +84,7 @@
 fun is_empty Empty = true
   | is_empty _ = false;
 
-fun is_single (Branch2 (Empty, _, Empty)) = true
+fun is_single (Leaf1 _) = true
   | is_single _ = false;
 
 
@@ -78,6 +93,8 @@
 fun fold_set f =
   let
     fun fold Empty x = x
+      | fold (Leaf1 e) x = f e x
+      | fold (Leaf2 (e1, e2)) x = f e2 (f e1 x)
       | fold (Branch2 (left, e, right)) x =
           fold right (f e (fold left x))
       | fold (Branch3 (left, e1, mid, e2, right)) x =
@@ -87,6 +104,8 @@
 fun fold_rev_set f =
   let
     fun fold_rev Empty x = x
+      | fold_rev (Leaf1 e) x = f e x
+      | fold_rev (Leaf2 (e1, e2)) x = f e1 (f e2 x)
       | fold_rev (Branch2 (left, e, right)) x =
           fold_rev left (f e (fold_rev right x))
       | fold_rev (Branch3 (left, e1, mid, e2, right)) x =
@@ -101,6 +120,8 @@
 fun exists pred =
   let
     fun ex Empty = false
+      | ex (Leaf1 e) = pred e
+      | ex (Leaf2 (e1, e2)) = pred e1 orelse pred e2
       | ex (Branch2 (left, e, right)) =
           ex left orelse pred e orelse ex right
       | ex (Branch3 (left, e1, mid, e2, right)) =
@@ -115,6 +136,11 @@
 fun get_first f =
   let
     fun get Empty = NONE
+      | get (Leaf1 e) = f e
+      | get (Leaf2 (e1, e2)) =
+          (case f e1 of
+            NONE => f e2
+          | some => some)
       | get (Branch2 (left, e, right)) =
           (case get left of
             NONE =>
@@ -143,6 +169,8 @@
 fun member set elem =
   let
     fun mem Empty = false
+      | mem (Leaf1 e) = eq_key (elem, e)
+      | mem (Leaf2 (e1, e2)) = eq_key (elem, e1) orelse eq_key (elem, e2)
       | mem (Branch2 (left, e, right)) =
           (case Key.ord (elem, e) of
             LESS => mem left
@@ -182,43 +210,45 @@
   else
     let
       fun ins Empty = Sprout (Empty, elem, Empty)
+        | ins (t as Leaf1 _) = ins (unmake t)
+        | ins (t as Leaf2 _) = ins (unmake t)
         | ins (Branch2 (left, e, right)) =
             (case Key.ord (elem, e) of
               LESS =>
                 (case ins left of
-                  Stay left' => Stay (Branch2 (left', e, right))
-                | Sprout (left1, e', left2) => Stay (Branch3 (left1, e', left2, e, right)))
-            | EQUAL => Stay (Branch2 (left, e, right))
+                  Stay left' => Stay (make2 (left', e, right))
+                | Sprout (left1, e', left2) => Stay (make3 (left1, e', left2, e, right)))
+            | EQUAL => Stay (make2 (left, e, right))
             | GREATER =>
                 (case ins right of
-                  Stay right' => Stay (Branch2 (left, e, right'))
+                  Stay right' => Stay (make2 (left, e, right'))
                 | Sprout (right1, e', right2) =>
-                    Stay (Branch3 (left, e, right1, e', right2))))
+                    Stay (make3 (left, e, right1, e', right2))))
         | ins (Branch3 (left, e1, mid, e2, right)) =
             (case Key.ord (elem, e1) of
               LESS =>
                 (case ins left of
-                  Stay left' => Stay (Branch3 (left', e1, mid, e2, right))
+                  Stay left' => Stay (make3 (left', e1, mid, e2, right))
                 | Sprout (left1, e', left2) =>
-                    Sprout (Branch2 (left1, e', left2), e1, Branch2 (mid, e2, right)))
-            | EQUAL => Stay (Branch3 (left, e1, mid, e2, right))
+                    Sprout (make2 (left1, e', left2), e1, make2 (mid, e2, right)))
+            | EQUAL => Stay (make3 (left, e1, mid, e2, right))
             | GREATER =>
                 (case Key.ord (elem, e2) of
                   LESS =>
                     (case ins mid of
-                      Stay mid' => Stay (Branch3 (left, e1, mid', e2, right))
+                      Stay mid' => Stay (make3 (left, e1, mid', e2, right))
                     | Sprout (mid1, e', mid2) =>
-                        Sprout (Branch2 (left, e1, mid1), e', Branch2 (mid2, e2, right)))
-                | EQUAL => Stay (Branch3 (left, e1, mid, e2, right))
+                        Sprout (make2 (left, e1, mid1), e', make2 (mid2, e2, right)))
+                | EQUAL => Stay (make3 (left, e1, mid, e2, right))
                 | GREATER =>
                     (case ins right of
-                      Stay right' => Stay (Branch3 (left, e1, mid, e2, right'))
+                      Stay right' => Stay (make3 (left, e1, mid, e2, right'))
                     | Sprout (right1, e', right2) =>
-                        Sprout (Branch2 (left, e1, mid), e2, Branch2 (right1, e', right2)))));
+                        Sprout (make2 (left, e1, mid), e2, make2 (right1, e', right2)))));
     in
       (case ins set of
         Stay set' => set'
-      | Sprout br => Branch2 br)
+      | Sprout br => make2 br)
     end;
 
 fun make elems = build (fold insert elems);
@@ -246,79 +276,78 @@
 (*literal copy from table.ML -- by Stefan Berghofer*)
 fun del (SOME k) Empty = raise UNDEF k
   | del NONE Empty = raise Match
-  | del NONE (Branch2 (Empty, p, Empty)) = (p, (true, Empty))
-  | del NONE (Branch3 (Empty, p, Empty, q, Empty)) =
-      (p, (false, Branch2 (Empty, q, Empty)))
-  | del k (Branch2 (Empty, p, Empty)) =
+  | del NONE (Leaf1 p) = (p, (true, Empty))
+  | del NONE (Leaf2 (p, q)) = (p, (false, Leaf1 q))
+  | del k (Leaf1 p) =
       (case compare k p of
         EQUAL => (p, (true, Empty))
       | _ => raise UNDEF (the k))
-  | del k (Branch3 (Empty, p, Empty, q, Empty)) =
+  | del k (Leaf2 (p, q)) =
       (case compare k p of
-        EQUAL => (p, (false, Branch2 (Empty, q, Empty)))
+        EQUAL => (p, (false, Leaf1 q))
       | _ =>
         (case compare k q of
-          EQUAL => (q, (false, Branch2 (Empty, p, Empty)))
+          EQUAL => (q, (false, Leaf1 p))
         | _ => raise UNDEF (the k)))
   | del k (Branch2 (l, p, r)) =
       (case compare k p of
         LESS =>
           (case del k l of
-            (p', (false, l')) => (p', (false, Branch2 (l', p, r)))
-          | (p', (true, l')) => (p', case r of
+            (p', (false, l')) => (p', (false, make2 (l', p, r)))
+          | (p', (true, l')) => (p', case unmake r of
               Branch2 (rl, rp, rr) =>
-                (true, Branch3 (l', p, rl, rp, rr))
-            | Branch3 (rl, rp, rm, rq, rr) => (false, Branch2
-                (Branch2 (l', p, rl), rp, Branch2 (rm, rq, rr)))))
+                (true, make3 (l', p, rl, rp, rr))
+            | Branch3 (rl, rp, rm, rq, rr) => (false, make2
+                (make2 (l', p, rl), rp, make2 (rm, rq, rr)))))
       | ord =>
           (case del (if_eq ord NONE k) r of
-            (p', (false, r')) => (p', (false, Branch2 (l, if_eq ord p' p, r')))
-          | (p', (true, r')) => (p', case l of
+            (p', (false, r')) => (p', (false, make2 (l, if_eq ord p' p, r')))
+          | (p', (true, r')) => (p', case unmake l of
               Branch2 (ll, lp, lr) =>
-                (true, Branch3 (ll, lp, lr, if_eq ord p' p, r'))
-            | Branch3 (ll, lp, lm, lq, lr) => (false, Branch2
-                (Branch2 (ll, lp, lm), lq, Branch2 (lr, if_eq ord p' p, r'))))))
+                (true, make3 (ll, lp, lr, if_eq ord p' p, r'))
+            | Branch3 (ll, lp, lm, lq, lr) => (false, make2
+                (make2 (ll, lp, lm), lq, make2 (lr, if_eq ord p' p, r'))))))
   | del k (Branch3 (l, p, m, q, r)) =
       (case compare k q of
         LESS =>
           (case compare k p of
             LESS =>
               (case del k l of
-                (p', (false, l')) => (p', (false, Branch3 (l', p, m, q, r)))
-              | (p', (true, l')) => (p', (false, case (m, r) of
+                (p', (false, l')) => (p', (false, make3 (l', p, m, q, r)))
+              | (p', (true, l')) => (p', (false, case (unmake m, unmake r) of
                   (Branch2 (ml, mp, mr), Branch2 _) =>
-                    Branch2 (Branch3 (l', p, ml, mp, mr), q, r)
+                    make2 (make3 (l', p, ml, mp, mr), q, r)
                 | (Branch3 (ml, mp, mm, mq, mr), _) =>
-                    Branch3 (Branch2 (l', p, ml), mp, Branch2 (mm, mq, mr), q, r)
+                    make3 (make2 (l', p, ml), mp, make2 (mm, mq, mr), q, r)
                 | (Branch2 (ml, mp, mr), Branch3 (rl, rp, rm, rq, rr)) =>
-                    Branch3 (Branch2 (l', p, ml), mp, Branch2 (mr, q, rl), rp,
-                      Branch2 (rm, rq, rr)))))
+                    make3 (make2 (l', p, ml), mp, make2 (mr, q, rl), rp,
+                      make2 (rm, rq, rr)))))
           | ord =>
               (case del (if_eq ord NONE k) m of
                 (p', (false, m')) =>
-                  (p', (false, Branch3 (l, if_eq ord p' p, m', q, r)))
-              | (p', (true, m')) => (p', (false, case (l, r) of
+                  (p', (false, make3 (l, if_eq ord p' p, m', q, r)))
+              | (p', (true, m')) => (p', (false, case (unmake l, unmake r) of
                   (Branch2 (ll, lp, lr), Branch2 _) =>
-                    Branch2 (Branch3 (ll, lp, lr, if_eq ord p' p, m'), q, r)
+                    make2 (make3 (ll, lp, lr, if_eq ord p' p, m'), q, r)
                 | (Branch3 (ll, lp, lm, lq, lr), _) =>
-                    Branch3 (Branch2 (ll, lp, lm), lq,
-                      Branch2 (lr, if_eq ord p' p, m'), q, r)
+                    make3 (make2 (ll, lp, lm), lq,
+                      make2 (lr, if_eq ord p' p, m'), q, r)
                 | (_, Branch3 (rl, rp, rm, rq, rr)) =>
-                    Branch3 (l, if_eq ord p' p, Branch2 (m', q, rl), rp,
-                      Branch2 (rm, rq, rr))))))
+                    make3 (l, if_eq ord p' p, make2 (m', q, rl), rp,
+                      make2 (rm, rq, rr))))))
       | ord =>
           (case del (if_eq ord NONE k) r of
             (q', (false, r')) =>
-              (q', (false, Branch3 (l, p, m, if_eq ord q' q, r')))
-          | (q', (true, r')) => (q', (false, case (l, m) of
+              (q', (false, make3 (l, p, m, if_eq ord q' q, r')))
+          | (q', (true, r')) => (q', (false, case (unmake l, unmake m) of
               (Branch2 _, Branch2 (ml, mp, mr)) =>
-                Branch2 (l, p, Branch3 (ml, mp, mr, if_eq ord q' q, r'))
+                make2 (l, p, make3 (ml, mp, mr, if_eq ord q' q, r'))
             | (_, Branch3 (ml, mp, mm, mq, mr)) =>
-                Branch3 (l, p, Branch2 (ml, mp, mm), mq,
-                  Branch2 (mr, if_eq ord q' q, r'))
+                make3 (l, p, make2 (ml, mp, mm), mq,
+                  make2 (mr, if_eq ord q' q, r'))
             | (Branch3 (ll, lp, lm, lq, lr), Branch2 (ml, mp, mr)) =>
-                Branch3 (Branch2 (ll, lp, lm), lq, Branch2 (lr, p, ml), mp,
-                  Branch2 (mr, if_eq ord q' q, r'))))));
+                make3 (make2 (ll, lp, lm), lq, make2 (lr, p, ml), mp,
+                  make2 (mr, if_eq ord q' q, r'))))));
 
 in
 
diff -r be3f838b3e17 -r 570f1436fe0a src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Tue Mar 28 19:43:49 2023 +0200
+++ b/src/Pure/General/table.ML	Tue Mar 28 22:43:05 2023 +0200
@@ -72,6 +72,8 @@
 structure Key = Key;
 type key = Key.key;
 
+val eq_key = is_equal o Key.ord;
+
 exception DUP of key;
 
 
@@ -79,9 +81,21 @@
 
 datatype 'a table =
   Empty |
+  Leaf1 of key * 'a |
+  Leaf2 of (key * 'a) * (key * 'a) |
   Branch2 of 'a table * (key * 'a) * 'a table |
   Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;
 
+fun make2 (Empty, e, Empty) = Leaf1 e
+  | make2 arg = Branch2 arg;
+
+fun make3 (Empty, e1, Empty, e2, Empty) = Leaf2 (e1, e2)
+  | make3 arg = Branch3 arg;
+
+fun unmake (Leaf1 e) = Branch2 (Empty, e, Empty)
+  | unmake (Leaf2 (e1, e2)) = Branch3 (Empty, e1, Empty, e2, Empty)
+  | unmake arg = arg;
+
 
 (* empty and single *)
 
@@ -92,7 +106,7 @@
 fun is_empty Empty = true
   | is_empty _ = false;
 
-fun is_single (Branch2 (Empty, _, Empty)) = true
+fun is_single (Leaf1 _) = true
   | is_single _ = false;
 
 
@@ -101,6 +115,8 @@
 fun map_table f =
   let
     fun map Empty = Empty
+      | map (Leaf1 (k, x)) = Leaf1 (k, f k x)
+      | map (Leaf2 ((k1, x1), (k2, x2))) = Leaf2 ((k1, f k1 x1), (k2, f k2 x2))
       | map (Branch2 (left, (k, x), right)) =
           Branch2 (map left, (k, f k x), map right)
       | map (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
@@ -110,6 +126,8 @@
 fun fold_table f =
   let
     fun fold Empty x = x
+      | fold (Leaf1 e) x = f e x
+      | fold (Leaf2 (e1, e2)) x = f e2 (f e1 x)
       | fold (Branch2 (left, e, right)) x =
           fold right (f e (fold left x))
       | fold (Branch3 (left, e1, mid, e2, right)) x =
@@ -119,6 +137,8 @@
 fun fold_rev_table f =
   let
     fun fold_rev Empty x = x
+      | fold_rev (Leaf1 e) x = f e x
+      | fold_rev (Leaf2 (e1, e2)) x = f e1 (f e2 x)
       | fold_rev (Branch2 (left, e, right)) x =
           fold_rev left (f e (fold_rev right x))
       | fold_rev (Branch3 (left, e1, mid, e2, right)) x =
@@ -132,12 +152,16 @@
 (* min/max entries *)
 
 fun min Empty = NONE
+  | min (Leaf1 e) = SOME e
+  | min (Leaf2 (e, _)) = SOME e
   | min (Branch2 (Empty, e, _)) = SOME e
   | min (Branch3 (Empty, e, _, _, _)) = SOME e
   | min (Branch2 (left, _, _)) = min left
   | min (Branch3 (left, _, _, _, _)) = min left;
 
 fun max Empty = NONE
+  | max (Leaf1 e) = SOME e
+  | max (Leaf2 (_, e)) = SOME e
   | max (Branch2 (_, e, Empty)) = SOME e
   | max (Branch3 (_, _, _, e, Empty)) = SOME e
   | max (Branch2 (_, _, right)) = max right
@@ -149,6 +173,8 @@
 fun exists pred =
   let
     fun ex Empty = false
+      | ex (Leaf1 e) = pred e
+      | ex (Leaf2 (e1, e2)) = pred e1 orelse pred e2
       | ex (Branch2 (left, e, right)) =
           ex left orelse pred e orelse ex right
       | ex (Branch3 (left, e1, mid, e2, right)) =
@@ -163,6 +189,11 @@
 fun get_first f =
   let
     fun get Empty = NONE
+      | get (Leaf1 e) = f e
+      | get (Leaf2 (e1, e2)) =
+          (case f e1 of
+            NONE => f e2
+          | some => some)
       | get (Branch2 (left, e, right)) =
           (case get left of
             NONE =>
@@ -191,6 +222,11 @@
 fun lookup tab key =
   let
     fun look Empty = NONE
+      | look (Leaf1 (k, x)) =
+          if eq_key (key, k) then SOME x else NONE
+      | look (Leaf2 ((k1, x1), (k2, x2))) =
+          if eq_key (key, k1) then SOME x1 else
+          if eq_key (key, k2) then SOME x2 else NONE
       | look (Branch2 (left, (k, x), right)) =
           (case Key.ord (key, k) of
             LESS => look left
@@ -210,6 +246,11 @@
 fun lookup_key tab key =
   let
     fun look Empty = NONE
+      | look (Leaf1 (k, x)) =
+          if eq_key (key, k) then SOME (k, x) else NONE
+      | look (Leaf2 ((k1, x1), (k2, x2))) =
+          if eq_key (key, k1) then SOME (k1, x1) else
+          if eq_key (key, k2) then SOME (k2, x2) else NONE
       | look (Branch2 (left, (k, x), right)) =
           (case Key.ord (key, k) of
             LESS => look left
@@ -229,6 +270,8 @@
 fun defined tab key =
   let
     fun def Empty = false
+      | def (Leaf1 (k, _)) = eq_key (key, k)
+      | def (Leaf2 ((k1, _), (k2, _))) = eq_key (key, k1) orelse eq_key (key, k2)
       | def (Branch2 (left, (k, _), right)) =
           (case Key.ord (key, k) of
             LESS => def left
@@ -257,44 +300,46 @@
 fun modify key f tab =
   let
     fun modfy Empty = Sprout (Empty, (key, f NONE), Empty)
+      | modfy (t as Leaf1 _) = modfy (unmake t)
+      | modfy (t as Leaf2 _) = modfy (unmake t)
       | modfy (Branch2 (left, p as (k, x), right)) =
           (case Key.ord (key, k) of
             LESS =>
               (case modfy left of
-                Stay left' => Stay (Branch2 (left', p, right))
-              | Sprout (left1, q, left2) => Stay (Branch3 (left1, q, left2, p, right)))
-          | EQUAL => Stay (Branch2 (left, (k, f (SOME x)), right))
+                Stay left' => Stay (make2 (left', p, right))
+              | Sprout (left1, q, left2) => Stay (make3 (left1, q, left2, p, right)))
+          | EQUAL => Stay (make2 (left, (k, f (SOME x)), right))
           | GREATER =>
               (case modfy right of
-                Stay right' => Stay (Branch2 (left, p, right'))
+                Stay right' => Stay (make2 (left, p, right'))
               | Sprout (right1, q, right2) =>
-                  Stay (Branch3 (left, p, right1, q, right2))))
+                  Stay (make3 (left, p, right1, q, right2))))
       | modfy (Branch3 (left, p1 as (k1, x1), mid, p2 as (k2, x2), right)) =
           (case Key.ord (key, k1) of
             LESS =>
               (case modfy left of
-                Stay left' => Stay (Branch3 (left', p1, mid, p2, right))
+                Stay left' => Stay (make3 (left', p1, mid, p2, right))
               | Sprout (left1, q, left2) =>
-                  Sprout (Branch2 (left1, q, left2), p1, Branch2 (mid, p2, right)))
-          | EQUAL => Stay (Branch3 (left, (k1, f (SOME x1)), mid, p2, right))
+                  Sprout (make2 (left1, q, left2), p1, make2 (mid, p2, right)))
+          | EQUAL => Stay (make3 (left, (k1, f (SOME x1)), mid, p2, right))
           | GREATER =>
               (case Key.ord (key, k2) of
                 LESS =>
                   (case modfy mid of
-                    Stay mid' => Stay (Branch3 (left, p1, mid', p2, right))
+                    Stay mid' => Stay (make3 (left, p1, mid', p2, right))
                   | Sprout (mid1, q, mid2) =>
-                      Sprout (Branch2 (left, p1, mid1), q, Branch2 (mid2, p2, right)))
-              | EQUAL => Stay (Branch3 (left, p1, mid, (k2, f (SOME x2)), right))
+                      Sprout (make2 (left, p1, mid1), q, make2 (mid2, p2, right)))
+              | EQUAL => Stay (make3 (left, p1, mid, (k2, f (SOME x2)), right))
               | GREATER =>
                   (case modfy right of
-                    Stay right' => Stay (Branch3 (left, p1, mid, p2, right'))
+                    Stay right' => Stay (make3 (left, p1, mid, p2, right'))
                   | Sprout (right1, q, right2) =>
-                      Sprout (Branch2 (left, p1, mid), p2, Branch2 (right1, q, right2)))));
+                      Sprout (make2 (left, p1, mid), p2, make2 (right1, q, right2)))));
 
   in
     (case modfy tab of
       Stay tab' => tab'
-    | Sprout br => Branch2 br)
+    | Sprout br => make2 br)
     handle SAME => tab
   end;
 
@@ -318,79 +363,78 @@
 
 fun del (SOME k) Empty = raise UNDEF k
   | del NONE Empty = raise Match
-  | del NONE (Branch2 (Empty, p, Empty)) = (p, (true, Empty))
-  | del NONE (Branch3 (Empty, p, Empty, q, Empty)) =
-      (p, (false, Branch2 (Empty, q, Empty)))
-  | del k (Branch2 (Empty, p, Empty)) =
+  | del NONE (Leaf1 p) = (p, (true, Empty))
+  | del NONE (Leaf2 (p, q)) = (p, (false, Leaf1 q))
+  | del k (Leaf1 p) =
       (case compare k p of
         EQUAL => (p, (true, Empty))
       | _ => raise UNDEF (the k))
-  | del k (Branch3 (Empty, p, Empty, q, Empty)) =
+  | del k (Leaf2 (p, q)) =
       (case compare k p of
-        EQUAL => (p, (false, Branch2 (Empty, q, Empty)))
+        EQUAL => (p, (false, Leaf1 q))
       | _ =>
         (case compare k q of
-          EQUAL => (q, (false, Branch2 (Empty, p, Empty)))
+          EQUAL => (q, (false, Leaf1 p))
         | _ => raise UNDEF (the k)))
   | del k (Branch2 (l, p, r)) =
       (case compare k p of
         LESS =>
           (case del k l of
-            (p', (false, l')) => (p', (false, Branch2 (l', p, r)))
-          | (p', (true, l')) => (p', case r of
+            (p', (false, l')) => (p', (false, make2 (l', p, r)))
+          | (p', (true, l')) => (p', case unmake r of
               Branch2 (rl, rp, rr) =>
-                (true, Branch3 (l', p, rl, rp, rr))
-            | Branch3 (rl, rp, rm, rq, rr) => (false, Branch2
-                (Branch2 (l', p, rl), rp, Branch2 (rm, rq, rr)))))
+                (true, make3 (l', p, rl, rp, rr))
+            | Branch3 (rl, rp, rm, rq, rr) => (false, make2
+                (make2 (l', p, rl), rp, make2 (rm, rq, rr)))))
       | ord =>
           (case del (if_eq ord NONE k) r of
-            (p', (false, r')) => (p', (false, Branch2 (l, if_eq ord p' p, r')))
-          | (p', (true, r')) => (p', case l of
+            (p', (false, r')) => (p', (false, make2 (l, if_eq ord p' p, r')))
+          | (p', (true, r')) => (p', case unmake l of
               Branch2 (ll, lp, lr) =>
-                (true, Branch3 (ll, lp, lr, if_eq ord p' p, r'))
-            | Branch3 (ll, lp, lm, lq, lr) => (false, Branch2
-                (Branch2 (ll, lp, lm), lq, Branch2 (lr, if_eq ord p' p, r'))))))
+                (true, make3 (ll, lp, lr, if_eq ord p' p, r'))
+            | Branch3 (ll, lp, lm, lq, lr) => (false, make2
+                (make2 (ll, lp, lm), lq, make2 (lr, if_eq ord p' p, r'))))))
   | del k (Branch3 (l, p, m, q, r)) =
       (case compare k q of
         LESS =>
           (case compare k p of
             LESS =>
               (case del k l of
-                (p', (false, l')) => (p', (false, Branch3 (l', p, m, q, r)))
-              | (p', (true, l')) => (p', (false, case (m, r) of
+                (p', (false, l')) => (p', (false, make3 (l', p, m, q, r)))
+              | (p', (true, l')) => (p', (false, case (unmake m, unmake r) of
                   (Branch2 (ml, mp, mr), Branch2 _) =>
-                    Branch2 (Branch3 (l', p, ml, mp, mr), q, r)
+                    make2 (make3 (l', p, ml, mp, mr), q, r)
                 | (Branch3 (ml, mp, mm, mq, mr), _) =>
-                    Branch3 (Branch2 (l', p, ml), mp, Branch2 (mm, mq, mr), q, r)
+                    make3 (make2 (l', p, ml), mp, make2 (mm, mq, mr), q, r)
                 | (Branch2 (ml, mp, mr), Branch3 (rl, rp, rm, rq, rr)) =>
-                    Branch3 (Branch2 (l', p, ml), mp, Branch2 (mr, q, rl), rp,
-                      Branch2 (rm, rq, rr)))))
+                    make3 (make2 (l', p, ml), mp, make2 (mr, q, rl), rp,
+                      make2 (rm, rq, rr)))))
           | ord =>
               (case del (if_eq ord NONE k) m of
                 (p', (false, m')) =>
-                  (p', (false, Branch3 (l, if_eq ord p' p, m', q, r)))
-              | (p', (true, m')) => (p', (false, case (l, r) of
+                  (p', (false, make3 (l, if_eq ord p' p, m', q, r)))
+              | (p', (true, m')) => (p', (false, case (unmake l, unmake r) of
                   (Branch2 (ll, lp, lr), Branch2 _) =>
-                    Branch2 (Branch3 (ll, lp, lr, if_eq ord p' p, m'), q, r)
+                    make2 (make3 (ll, lp, lr, if_eq ord p' p, m'), q, r)
                 | (Branch3 (ll, lp, lm, lq, lr), _) =>
-                    Branch3 (Branch2 (ll, lp, lm), lq,
-                      Branch2 (lr, if_eq ord p' p, m'), q, r)
+                    make3 (make2 (ll, lp, lm), lq,
+                      make2 (lr, if_eq ord p' p, m'), q, r)
                 | (_, Branch3 (rl, rp, rm, rq, rr)) =>
-                    Branch3 (l, if_eq ord p' p, Branch2 (m', q, rl), rp,
-                      Branch2 (rm, rq, rr))))))
+                    make3 (l, if_eq ord p' p, make2 (m', q, rl), rp,
+                      make2 (rm, rq, rr))))))
       | ord =>
           (case del (if_eq ord NONE k) r of
             (q', (false, r')) =>
-              (q', (false, Branch3 (l, p, m, if_eq ord q' q, r')))
-          | (q', (true, r')) => (q', (false, case (l, m) of
+              (q', (false, make3 (l, p, m, if_eq ord q' q, r')))
+          | (q', (true, r')) => (q', (false, case (unmake l, unmake m) of
               (Branch2 _, Branch2 (ml, mp, mr)) =>
-                Branch2 (l, p, Branch3 (ml, mp, mr, if_eq ord q' q, r'))
+                make2 (l, p, make3 (ml, mp, mr, if_eq ord q' q, r'))
             | (_, Branch3 (ml, mp, mm, mq, mr)) =>
-                Branch3 (l, p, Branch2 (ml, mp, mm), mq,
-                  Branch2 (mr, if_eq ord q' q, r'))
+                make3 (l, p, make2 (ml, mp, mm), mq,
+                  make2 (mr, if_eq ord q' q, r'))
             | (Branch3 (ll, lp, lm, lq, lr), Branch2 (ml, mp, mr)) =>
-                Branch3 (Branch2 (ll, lp, lm), lq, Branch2 (lr, p, ml), mp,
-                  Branch2 (mr, if_eq ord q' q, r'))))));
+                make3 (make2 (ll, lp, lm), lq, make2 (lr, p, ml), mp,
+                  make2 (mr, if_eq ord q' q, r'))))));
 
 in