# HG changeset patch
# User nipkow
# Date 1485516769 -3600
# Node ID 140addd19343010186e4c0708871aff5c7d160f9
# Parent  10b8d31634cc0f5f5d1442d46d01ca201d95d13d
removed contribution by Daniel Stuewe, too detailed.

diff -r 10b8d31634cc -r 140addd19343 src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Thu Jan 26 17:51:13 2017 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Fri Jan 27 12:32:49 2017 +0100
@@ -1,4 +1,4 @@
-(* Author: Tobias Nipkow, Daniel Stüwe *)
+(* Author: Tobias Nipkow *)
 
 section \<open>Red-Black Tree Implementation of Sets\<close>
 
@@ -99,7 +99,7 @@
 
 fun bheight :: "'a rbt \<Rightarrow> nat" where
 "bheight Leaf = 0" |
-"bheight (Node c l x r) = (if c = Black then Suc(bheight l) else bheight l)"
+"bheight (Node c l x r) = (if c = Black then bheight l + 1 else bheight l)"
 
 fun invc :: "'a rbt \<Rightarrow> bool" where
 "invc Leaf = True" |