# HG changeset patch
# User wenzelm
# Date 1681907392 -7200
# Node ID bb7238e7d2d90c17e43dbef077a6a7a99f8240dc
# Parent  560bdb9f2101844a5e7e947ec3e403cc9c044d2e
minor performance tuning: avoid excessive (de)constructions for base cases;

diff -r 560bdb9f2101 -r bb7238e7d2d9 src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Wed Apr 19 11:10:52 2023 +0200
+++ b/src/Pure/General/set.ML	Wed Apr 19 14:29:52 2023 +0200
@@ -287,7 +287,8 @@
   if member set elem then set
   else
     let
-      fun elem_ord e = Key.ord (elem, e)
+      fun elem_ord e = Key.ord (elem, e);
+      fun elem_less e = elem_ord e = LESS;
 
       fun ins Empty = Sprout (Empty, elem, Empty)
         | ins (t as Leaf1 _) = ins (unmake t)
@@ -328,10 +329,23 @@
                         Sprout (make2 (left, e1, mid), e2, make2 (right1, e', right2)))))
         | ins (Size (_, arg)) = ins arg;
     in
-      make_size (size set + 1)
-        (case ins set of
-          Stay set' => set'
-        | Sprout br => make2 br)
+      (case set of
+        Empty => Leaf1 elem
+      | Leaf1 e =>
+          if elem_less e
+          then Leaf2 (elem, e)
+          else Leaf2 (e, elem)
+      | Leaf2 (e1, e2) =>
+          if elem_less e1
+          then Leaf3 (elem, e1, e2)
+          else if elem_less e2
+          then Leaf3 (e1, elem, e2)
+          else Leaf3 (e1, e2, elem)
+      | _ =>
+          make_size (size set + 1)
+            (case ins set of
+              Stay set' => set'
+            | Sprout br => make2 br))
     end;
 
 fun make elems = build (fold insert elems);
diff -r 560bdb9f2101 -r bb7238e7d2d9 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Wed Apr 19 11:10:52 2023 +0200
+++ b/src/Pure/General/table.ML	Wed Apr 19 14:29:52 2023 +0200
@@ -454,9 +454,26 @@
       | modfy (Size (_, arg)) = modfy arg;
 
     val tab' =
-      (case modfy tab of
-        Stay tab' => tab'
-      | Sprout br => make2 br);
+      (case tab of
+        Empty => Leaf1 (key, insert ())
+      | Leaf1 (k, x) =>
+          (case key_ord k of
+            LESS => Leaf2 (key, insert (), k, x)
+          | EQUAL => Leaf1 (k, update x)
+          | GREATER => Leaf2 (k, x, key, insert ()))
+      | Leaf2 (k1, x1, k2, x2) =>
+          (case key_ord k1 of
+            LESS => Leaf3 (key, insert (), k1, x1, k2, x2)
+          | EQUAL => Leaf2 (k1, update x1, k2, x2)
+          | GREATER =>
+              (case key_ord k2 of
+                LESS => Leaf3 (k1, x1, key, insert (), k2, x2)
+              | EQUAL => Leaf2 (k1, x1, k2, update x2)
+              | GREATER => Leaf3 (k1, x1, k2, x2, key, insert ())))
+      | _ =>
+          (case modfy tab of
+            Stay tab' => tab'
+          | Sprout br => make2 br));
   in
     make_size (size tab + !inc) tab'
   end handle SAME => tab;