# HG changeset patch
# User nipkow
# Date 1577488543 -3600
# Node ID 857453c0db3d7d4924c08ce328530dc986e45e4b
# Parent  3c4c171344f483f5a08b6f7c7244825a5bf02574
tuned

diff -r 3c4c171344f4 -r 857453c0db3d src/HOL/Data_Structures/RBT.thy
--- a/src/HOL/Data_Structures/RBT.thy	Fri Dec 27 16:02:23 2019 +0100
+++ b/src/HOL/Data_Structures/RBT.thy	Sat Dec 28 00:15:43 2019 +0100
@@ -48,7 +48,7 @@
      t23 \<Rightarrow> R t1 a (R t23 c t4))" |
 "combine (B t1 a t2) (B t3 c t4) =
   (case combine t2 t3 of
-     R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) |
+     R u2 b u3 \<Rightarrow> R (B t1 a u2) b (B u3 c t4) |
      t23 \<Rightarrow> baldL t1 a (B t23 c t4))" |
 "combine t1 (R t2 a t3) = R (combine t1 t2) a t3" |
 "combine (R t1 a t2) t3 = R t1 a (combine t2 t3)" 
diff -r 3c4c171344f4 -r 857453c0db3d src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Fri Dec 27 16:02:23 2019 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Sat Dec 28 00:15:43 2019 +0100
@@ -195,7 +195,7 @@
 
 lemma invh_baldL_invc:
   "\<lbrakk> invh l;  invh r;  bheight l + 1 = bheight r;  invc r \<rbrakk>
-   \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight l + 1"
+   \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight r"
 by (induct l a r rule: baldL.induct)
    (auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red)