# HG changeset patch
# User wenzelm
# Date 1679927094 -7200
# Node ID 7c1cc9ce9340925f5f4ee06e721ff0175f7c00e9
# Parent  f750047e93861fba501f34e4ab7f327e57925bfc
tuned whitespace;

diff -r f750047e9386 -r 7c1cc9ce9340 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Mon Mar 27 11:52:10 2023 +0200
+++ b/src/Pure/General/table.ML	Mon Mar 27 16:24:54 2023 +0200
@@ -317,64 +317,76 @@
   | 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)) = (case compare k p of
-      EQUAL => (p, (true, Empty)) | _ => raise UNDEF (the k))
-  | del k (Branch3 (Empty, p, Empty, q, Empty)) = (case compare k p of
-      EQUAL => (p, (false, Branch2 (Empty, q, Empty)))
-    | _ => (case compare k q of
-        EQUAL => (q, (false, Branch2 (Empty, p, Empty)))
-      | _ => 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
-          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)))))
-    | 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
-          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'))))))
-  | 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
-            (Branch2 (ml, mp, mr), Branch2 _) =>
-              Branch2 (Branch3 (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)
-          | (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)))))
-      | 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
-            (Branch2 (ll, lp, lr), Branch2 _) =>
-              Branch2 (Branch3 (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)
-          | (_, Branch3 (rl, rp, rm, rq, rr)) =>
-              Branch3 (l, if_eq ord p' p, Branch2 (m', q, rl), rp,
-                Branch2 (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
-          (Branch2 _, Branch2 (ml, mp, mr)) =>
-            Branch2 (l, p, Branch3 (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'))
-        | (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'))))));
+  | del k (Branch2 (Empty, p, Empty)) =
+      (case compare k p of
+        EQUAL => (p, (true, Empty))
+      | _ => raise UNDEF (the k))
+  | del k (Branch3 (Empty, p, Empty, q, Empty)) =
+      (case compare k p of
+        EQUAL => (p, (false, Branch2 (Empty, q, Empty)))
+      | _ =>
+        (case compare k q of
+          EQUAL => (q, (false, Branch2 (Empty, p, Empty)))
+        | _ => 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
+              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)))))
+      | 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
+              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'))))))
+  | 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
+                  (Branch2 (ml, mp, mr), Branch2 _) =>
+                    Branch2 (Branch3 (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)
+                | (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)))))
+          | 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
+                  (Branch2 (ll, lp, lr), Branch2 _) =>
+                    Branch2 (Branch3 (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)
+                | (_, Branch3 (rl, rp, rm, rq, rr)) =>
+                    Branch3 (l, if_eq ord p' p, Branch2 (m', q, rl), rp,
+                      Branch2 (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
+              (Branch2 _, Branch2 (ml, mp, mr)) =>
+                Branch2 (l, p, Branch3 (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'))
+            | (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'))))));
 
 in