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