diff -r b87b41ade3b2 -r deae80045527 doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Thu Jan 10 01:13:41 2002 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Thu Jan 10 11:22:03 2002 +0100
@@ -189,7 +189,7 @@
 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ }{\isasymforall}i{\isachardot}\ n\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i%
 \end{isabelle}
 After stripping the \isa{{\isasymforall}i}, the proof continues with a case
-distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}} is trivial and we focus on
+distinction on \isa{i}. The case \isa{i\ {\isacharequal}\ {\isadigit{0}}} is trivial and we focus on
 the other case:%
 \end{isamarkuptxt}%
 \isamarkuptrue%