diff -r 2e89bc578935 -r 1f1354ca7ea7 src/HOL/Data_Structures/Tree234.thy
--- a/src/HOL/Data_Structures/Tree234.thy	Thu Nov 19 10:05:46 2015 +0100
+++ b/src/HOL/Data_Structures/Tree234.thy	Thu Nov 19 18:43:41 2015 +0100
@@ -10,10 +10,11 @@
 fixes height :: "'a \<Rightarrow> nat"
 
 datatype 'a tree234 =
-  Leaf |
-  Node2 "'a tree234" 'a "'a tree234" |
-  Node3 "'a tree234" 'a "'a tree234" 'a "'a tree234" |
+  Leaf ("\<langle>\<rangle>") |
+  Node2 "'a tree234" 'a "'a tree234"  ("\<langle>_, _, _\<rangle>") |
+  Node3 "'a tree234" 'a "'a tree234" 'a "'a tree234"  ("\<langle>_, _, _, _, _\<rangle>") |
   Node4 "'a tree234" 'a "'a tree234" 'a "'a tree234" 'a "'a tree234"
+    ("\<langle>_, _, _, _, _, _, _\<rangle>")
 
 fun inorder :: "'a tree234 \<Rightarrow> 'a list" where
 "inorder Leaf = []" |