--- a/doc-src/TutorialI/Recdef/termination.thy Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/Recdef/termination.thy Wed Dec 12 09:04:20 2001 +0100
@@ -48,7 +48,7 @@
(*<*)local(*>*)
text{*\noindent
This time everything works fine. Now @{thm[source]f.simps} contains precisely
-the stated recursion equation for @{term f}, which has been stored as a
+the stated recursion equation for @{text f}, which has been turned into a
simplification rule. Thus we can automatically prove results such as this one:
*}