--- 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%