--- a/doc-src/TutorialI/Datatype/Nested.thy Fri Nov 02 08:26:01 2007 +0100
+++ b/doc-src/TutorialI/Datatype/Nested.thy Fri Nov 02 08:59:15 2007 +0100
@@ -149,9 +149,9 @@
@{text term} are still awkward because they expect a conjunction. One
could derive a new induction principle as well (see
\S\ref{sec:derive-ind}), but simpler is to stop using \isacommand{primrec}
-and to define functions with \isacommand{recdef} instead.
-Simple uses of \isacommand{recdef} are described in \S\ref{sec:recdef} below,
-and later (\S\ref{sec:nested-recdef}) we shall see how \isacommand{recdef} can
+and to define functions with \isacommand{fun} instead.
+Simple uses of \isacommand{fun} are described in \S\ref{sec:fun} below,
+and later (\S\ref{sec:nested-recdef}) we shall see how \isacommand{fun} can
handle nested recursion.
Of course, you may also combine mutual and nested recursion of datatypes. For example,