author | nipkow |
Thu, 16 May 2019 12:59:37 +0200 | |
changeset 70272 | 1d564a895296 |
parent 70271 | f7630118814c |
child 70273 | acc1749c2be9 |
--- a/src/HOL/Data_Structures/Tree23_Set.thy Wed May 15 14:43:32 2019 +0100 +++ b/src/HOL/Data_Structures/Tree23_Set.thy Thu May 16 12:59:37 2019 +0200 @@ -128,7 +128,7 @@ (case cmp x a of LT \<Rightarrow> node21 (del x l) a r | GT \<Rightarrow> node22 l a (del x r) | - EQ \<Rightarrow> let (a',t) = split_min r in node22 l a' t)" | + EQ \<Rightarrow> let (a',r') = split_min r in node22 l a' r')" | "del x (Node3 l a m b r) = (case cmp x a of LT \<Rightarrow> node31 (del x l) a m b r |