diff -r 43ef6c6dd906 -r f88d0c363582 doc-src/TutorialI/Misc/Tree2.thy
--- a/doc-src/TutorialI/Misc/Tree2.thy	Fri Jul 05 11:47:44 2002 +0200
+++ b/doc-src/TutorialI/Misc/Tree2.thy	Fri Jul 05 17:48:05 2002 +0200
@@ -8,7 +8,7 @@
 quadratic. A linear time version of @{term"flatten"} again reqires an extra
 argument, the accumulator: *}
 
-consts flatten2 :: "'a tree => 'a list => 'a list"
+consts flatten2 :: "'a tree \<Rightarrow> 'a list \<Rightarrow> 'a list"
 (*<*)
 primrec
 "flatten2 Tip xs = xs"