diff -r 499637e8f2c6 -r 0376cccd9118 doc-src/TutorialI/Misc/document/Tree2.tex
--- a/doc-src/TutorialI/Misc/document/Tree2.tex	Wed Oct 11 09:09:06 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree2.tex	Wed Oct 11 10:44:42 2000 +0200
@@ -9,11 +9,11 @@
 quadratic. A linear time version of \isa{flatten} again reqires an extra
 argument, the accumulator:%
 \end{isamarkuptext}%
-\isacommand{consts}\ flatten\isadigit{2}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list{\isachardoublequote}%
+\isacommand{consts}\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list\ {\isacharequal}{\isachargreater}\ {\isacharprime}a\ list{\isachardoublequote}%
 \begin{isamarkuptext}%
-\noindent Define \isa{flatten\isadigit{2}} and prove%
+\noindent Define \isa{flatten{\isadigit{2}}} and prove%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}flatten\isadigit{2}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabellebody}%
+\isacommand{lemma}\ {\isachardoublequote}flatten{\isadigit{2}}\ t\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ flatten\ t{\isachardoublequote}\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"