diff -r ac8ca15c556c -r 885e053ae664 doc-src/TutorialI/Recdef/document/examples.tex
--- a/doc-src/TutorialI/Recdef/document/examples.tex	Mon Oct 08 12:13:34 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/examples.tex	Mon Oct 08 12:13:56 2001 +0200
@@ -8,7 +8,7 @@
 \isacommand{consts}\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
 \isacommand{recdef}\ fib\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
 \ \ {\isachardoublequote}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline
-\ \ {\isachardoublequote}fib\ {\isadigit{1}}{\isacharprime}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline
+\ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}\isanewline
 \ \ {\isachardoublequote}fib\ {\isacharparenleft}Suc{\isacharparenleft}Suc\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ x\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ x{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent