| changeset 77739 | 2225d3267f58 |
| parent 77737 | 81d553e9428d |
| child 77740 | 19c539f5d4d3 |
--- 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)