diff -r a8c707352ccc -r 59aefb3b9e95 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Thu Nov 01 09:25:58 2018 +0100
+++ b/src/HOL/Library/Tree.thy	Thu Nov 01 11:26:38 2018 +0100
@@ -9,9 +9,17 @@
 
 datatype 'a tree =
   Leaf ("\<langle>\<rangle>") |
-  Node "'a tree" (root_val: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
+  Node "'a tree" (root: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)")
 datatype_compat tree
 
+primrec left :: "'a tree \<Rightarrow> 'a tree" where
+"left (Node l v r) = l" |
+"left Leaf = Leaf"
+
+primrec right :: "'a tree \<Rightarrow> 'a tree" where
+"right (Node l v r) = r" |
+"right Leaf = Leaf"
+
 text\<open>Counting the number of leaves rather than nodes:\<close>
 
 fun size1 :: "'a tree \<Rightarrow> nat" where