src/Doc/Datatypes/Datatypes.thy

     ML {* Old_Datatype_Data.get_info @{theory} @{type_name even_nat} *}
 
 text {*
 The syntactic entity \synt{name} denotes an identifier \cite{isabelle-isar-ref}.
 
-The command is interesting because the old datatype package provides some
-functionality that is not yet replicated in the new package, such as the
-integration with Quickcheck.
+The command can be useful because the old datatype package provides some
+functionality that is not yet replicated in the new package.
 
 A few remarks concern nested recursive datatypes:
 
 \begin{itemize}
 \setlength{\itemsep}{0pt}

 
 \item All types through which recursion takes place must be new-style datatypes
 or the function type. In principle, it should be possible to support old-style
 datatypes as well, but this has not been implemented 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 might affect the behavior of
-some third-party extensions.
 \end{itemize}
 
 An alternative to @{command datatype_compat} is to use the old package's
 \keyw{rep_\allowbreak datatype} command. The associated proof obligations must then be
 discharged manually.