tuned
authornipkow
Thu May 16 12:59:37 2019 +0200 (4 days ago ago)
changeset 704561d564a895296
parent 70455 f7630118814c
child 70457 acc1749c2be9
tuned
src/HOL/Data_Structures/Tree23_Set.thy
     1.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Wed May 15 14:43:32 2019 +0100
     1.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Thu May 16 12:59:37 2019 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4    (case cmp x a of
     1.5       LT \<Rightarrow> node21 (del x l) a r |
     1.6       GT \<Rightarrow> node22 l a (del x r) |
     1.7 -     EQ \<Rightarrow> let (a',t) = split_min r in node22 l a' t)" |
     1.8 +     EQ \<Rightarrow> let (a',r') = split_min r in node22 l a' r')" |
     1.9  "del x (Node3 l a m b r) =
    1.10    (case cmp x a of
    1.11       LT \<Rightarrow> node31 (del x l) a m b r |