--- 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" |