# HG changeset patch
# User nipkow
# Date 1452674296 -3600
# Node ID ff20b44b2fc875f24f77eb6a32074f7902dcdd90
# Parent  adcaaf6c99104159515453058ab299ca5a3b217d
tuned layout

diff -r adcaaf6c9910 -r ff20b44b2fc8 src/HOL/Data_Structures/AA_Set.thy
--- a/src/HOL/Data_Structures/AA_Set.thy	Wed Jan 13 00:12:43 2016 +0100
+++ b/src/HOL/Data_Structures/AA_Set.thy	Wed Jan 13 09:38:16 2016 +0100
@@ -72,7 +72,7 @@
     else
       case r of
         Leaf \<Rightarrow> Leaf (* unreachable *) |
-        Node _ t1 b t4 \<Rightarrow>
+        Node lvb t1 b t4 \<Rightarrow>
           (case t1 of
              Node lva t2 a t3
                \<Rightarrow> Node (lva+1) (Node (lv-1) l x t2) a
diff -r adcaaf6c9910 -r ff20b44b2fc8 src/HOL/Data_Structures/Tree2.thy
--- a/src/HOL/Data_Structures/Tree2.thy	Wed Jan 13 00:12:43 2016 +0100
+++ b/src/HOL/Data_Structures/Tree2.thy	Wed Jan 13 09:38:16 2016 +0100
@@ -4,7 +4,7 @@
 
 datatype ('a,'b) tree =
   Leaf ("\<langle>\<rangle>") |
-  Node 'b "('a,'b)tree" 'a "('a,'b) tree" ("\<langle>_, _, _, _\<rangle>")
+  Node 'b "('a,'b)tree" 'a "('a,'b) tree" ("(1\<langle>_,/ _,/ _,/ _\<rangle>)")
 
 fun inorder :: "('a,'b)tree \<Rightarrow> 'a list" where
 "inorder Leaf = []" |
diff -r adcaaf6c9910 -r ff20b44b2fc8 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Wed Jan 13 00:12:43 2016 +0100
+++ b/src/HOL/Library/Tree.thy	Wed Jan 13 09:38:16 2016 +0100
@@ -7,8 +7,8 @@
 begin
 
 datatype 'a tree =
-  Leaf ("\<langle>\<rangle>") |
-  Node (left: "'a tree") (val: 'a) (right: "'a tree") ("\<langle>_, _, _\<rangle>")
+  is_Leaf: Leaf ("\<langle>\<rangle>") |
+  Node (left: "'a tree") (val: 'a) (right: "'a tree") ("(1\<langle>_,/ _,/ _\<rangle>)")
   where
     "left Leaf = Leaf"
   | "right Leaf = Leaf"