diff -r c1f3fa32d322 -r f02b4f41bfd6 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 08 14:03:01 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 08 14:03:01 2014 +0200 @@ -605,9 +605,8 @@ 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: @@ -622,10 +621,6 @@ 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