# HG changeset patch
# User nipkow
# Date 1577573066 -3600
# Node ID fb788bd799d98e45eb3ab9473fcd2c0dbd1f2436
# Parent  857453c0db3d7d4924c08ce328530dc986e45e4b
tuned

diff -r 857453c0db3d -r fb788bd799d9 src/HOL/Data_Structures/RBT.thy
--- a/src/HOL/Data_Structures/RBT.thy	Sat Dec 28 00:15:43 2019 +0100
+++ b/src/HOL/Data_Structures/RBT.thy	Sat Dec 28 23:44:26 2019 +0100
@@ -29,8 +29,8 @@
 
 fun baldL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
 "baldL (R t1 a t2) b t3 = R (B t1 a t2) b t3" |
-"baldL bl a (B t1 b t2) = baliR bl a (R t1 b t2)" |
-"baldL bl a (R (B t1 b t2) c t3) = R (B bl a t1) b (baliR t2 c (paint Red t3))" |
+"baldL t1 a (B t2 b t3) = baliR t1 a (R t2 b t3)" |
+"baldL t1 a (R (B t2 b t3) c t4) = R (B t1 a t2) b (baliR t3 c (paint Red t4))" |
 "baldL t1 a t2 = R t1 a t2"
 
 fun baldR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where