
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




