diff -r a5f53d9d2b60 -r f8537d69f514 doc-src/TutorialI/Misc/Tree.thy
--- a/doc-src/TutorialI/Misc/Tree.thy	Thu May 29 13:27:13 2008 +0200
+++ b/doc-src/TutorialI/Misc/Tree.thy	Thu May 29 22:45:33 2008 +0200
@@ -8,9 +8,8 @@
 
 datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)
 
-consts mirror :: "'a tree \<Rightarrow> 'a tree";
-primrec
-"mirror Tip = Tip"
+primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
+"mirror Tip = Tip" |
 "mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
 
 text{*\noindent
@@ -23,9 +22,8 @@
 apply(induct_tac t);
 by(auto);
 
-consts flatten :: "'a tree => 'a list"
-primrec
-"flatten Tip = []"
+primrec flatten :: "'a tree => 'a list" where
+"flatten Tip = []" |
 "flatten (Node l x r) = flatten l @ [x] @ flatten r";
 (*>*)