# HG changeset patch
# User nipkow
# Date 1537108316 -7200
# Node ID 2af022252782f5b2605e25d395d70b4257084024
# Parent  8188985565041f5a1a29244635e3a4c379e61971
tuned

diff -r 818898556504 -r 2af022252782 src/HOL/Library/Tree.thy
--- 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 ..