tuned

--- a/src/HOL/Library/Tree.thy	Sun Sep 16 15:16:04 2018 +0200
+++ b/src/HOL/Library/Tree.thy	Sun Sep 16 16:31:56 2018 +0200
@@ -33,7 +33,7 @@
 
 fun height_tree :: "'a tree => nat" where
 "height Leaf = 0" |
-"height (Node t1 a t2) = max (height t1) (height t2) + 1"
+"height (Node l a r) = max (height l) (height r) + 1"
 
 instance ..