diff -r 3307149f1ec2 -r f41e477576b9 doc-src/TutorialI/Recdef/document/termination.tex
--- a/doc-src/TutorialI/Recdef/document/termination.tex	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Wed Dec 12 09:04:20 2001 +0100
@@ -59,7 +59,7 @@
 \begin{isamarkuptext}%
 \noindent
 This time everything works fine. Now \isa{f{\isachardot}simps} contains precisely
-the stated recursion equation for \isa{{\isacharquery}{\isacharquery}{\isachardot}f}, which has been stored as a
+the stated recursion equation for \isa{f}, which has been turned into a
 simplification rule.  Thus we can automatically prove results such as this one:%
 \end{isamarkuptext}%
 \isamarkuptrue%