diff -r 7007bc8ddae4 -r 3a5d33e8a019 doc-src/TutorialI/Fun/fun0.thy
--- a/doc-src/TutorialI/Fun/fun0.thy	Fri Nov 02 16:38:14 2007 +0100
+++ b/doc-src/TutorialI/Fun/fun0.thy	Fri Nov 02 16:38:37 2007 +0100
@@ -105,7 +105,7 @@
 \subsection{Simplification}
 \label{sec:fun-simplification}
 
-Upon successful termination proof, the recursion equations become
+Upon a successful termination proof, the recursion equations become
 simplification rules, just as with \isacommand{primrec}.
 In most cases this works fine, but there is a subtle
 problem that must be mentioned: simplification may not