diff -r a6fb4ddc05c7 -r 0a4cc9b113c7 doc-src/TutorialI/Recdef/examples.thy
--- a/doc-src/TutorialI/Recdef/examples.thy	Mon May 02 10:56:13 2005 +0200
+++ b/doc-src/TutorialI/Recdef/examples.thy	Mon May 02 11:03:27 2005 +0200
@@ -63,7 +63,7 @@
 one does not match, Isabelle internally replaces the second equation
 by the two possibilities that are left: @{prop"sep1(a,[]) = []"} and
 @{prop"sep1(a, [x]) = [x]"}.  Thus the functions @{term sep} and
-@{term sep1} are identical.
+@{const sep1} are identical.
 
 \begin{warn}
   \isacommand{recdef} only takes the first argument of a (curried)