# HG changeset patch
# User nipkow
# Date 1558004377 -7200
# Node ID 1d564a895296e3ea3c8a35b321c131502a060fd9
# Parent  f7630118814cc6a449bb536e8e67edb887963b30
tuned

diff -r f7630118814c -r 1d564a895296 src/HOL/Data_Structures/Tree23_Set.thy
--- 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 |