# HG changeset patch
# User blanchet
# Date 1382344701 -7200
# Node ID 3fe73f3c84a2b35e68fa054bca0575a1b99b4216
# Parent  8a6a4938512250902a662d49fe70309e845af648
more docs

diff -r 8a6a49385122 -r 3fe73f3c84a2 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Oct 21 10:31:31 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Oct 21 10:38:21 2013 +0200
@@ -577,6 +577,10 @@
 or the function type. In principle, it should be possible to support old-style
 datatypes as well, but the command does not support this yet (and there is
 currently no way to register old-style datatypes as new-style datatypes).
+
+\item The recursor produced for types that recurse through functions has a
+different signature than with the old package. This makes it impossible to use
+the old \keyw{primrec} command.
 \end{itemize}
 
 An alternative to @{command datatype_new_compat} is to use the old package's
@@ -1022,9 +1026,10 @@
 
 text {*
 \noindent
-The next example is not primitive recursive, but it can be defined easily using
-\keyw{fun}. The @{command datatype_new_compat} command is needed to register
-new-style datatypes for use with \keyw{fun} and \keyw{function}
+The next example is defined using \keyw{fun} to escape the syntactic
+restrictions imposed on primitive recursive functions. The
+@{command datatype_new_compat} command is needed to register new-style datatypes
+for use with \keyw{fun} and \keyw{function}
 (Section~\ref{sssec:datatype-new-compat}):
 *}