# HG changeset patch
# User wenzelm
# Date 1680078890 -7200
# Node ID 2225d3267f58b92092dd75b93edf2a0c65a1b699
# Parent  e64428b6b170aa763adbda917f8f16bb9c87cc34
slightly more compact data;

diff -r e64428b6b170 -r 2225d3267f58 src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Tue Mar 28 23:16:27 2023 +0200
+++ b/src/Pure/General/set.ML	Wed Mar 29 10:34:50 2023 +0200
@@ -50,6 +50,8 @@
   Branch3 of T * elem * T * elem * T;
 
 fun make2 (Empty, e, Empty) = Leaf1 e
+  | make2 (Leaf1 e1, e2, Empty) = Leaf2 (e1, e2)
+  | make2 (Empty, e1, Leaf1 e2) = Leaf2 (e1, e2)
   | make2 arg = Branch2 arg;
 
 fun make3 (Empty, e1, Empty, e2, Empty) = Leaf2 (e1, e2)
diff -r e64428b6b170 -r 2225d3267f58 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Tue Mar 28 23:16:27 2023 +0200
+++ b/src/Pure/General/table.ML	Wed Mar 29 10:34:50 2023 +0200
@@ -87,6 +87,8 @@
   Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;
 
 fun make2 (Empty, e, Empty) = Leaf1 e
+  | make2 (Leaf1 e1, e2, Empty) = Leaf2 (e1, e2)
+  | make2 (Empty, e1, Leaf1 e2) = Leaf2 (e1, e2)
   | make2 arg = Branch2 arg;
 
 fun make3 (Empty, e1, Empty, e2, Empty) = Leaf2 (e1, e2)