--- 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)
--- 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)