diff -r e8472fc02fe5 -r 852f7a49ec0c src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Sun Apr 19 15:38:24 2015 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Sun Apr 19 19:29:38 2015 +0200
@@ -604,8 +604,8 @@
 text {*
 The syntactic entity \synt{name} denotes an identifier @{cite "isabelle-isar-ref"}.
 
-The command can be useful because the old datatype package provides some
-functionality that is not yet replicated in the new package.
+The command is sometimes useful when migrating from the old datatype package to
+the new one.
 
 A few remarks concern nested recursive datatypes:
 
@@ -1088,8 +1088,8 @@
 
 \item \emph{The Standard ML interfaces are different.} Tools and extensions
 written to call the old ML interfaces will need to be adapted to the new
-interfaces. If possible, it is recommended to register new-style datatypes as
-old-style datatypes using the @{command datatype_compat} command.
+interfaces. The @{text BNF_LFP_Compat} structure provides convenience functions
+that simulate the old interfaces in terms of the new ones.
 
 \item \emph{The recursor @{text rec_t} has a different signature for nested
 recursive datatypes.} In the old package, nested recursion through non-functions
@@ -1256,16 +1256,9 @@
   \qquad @{thm at_simps(2)[no_vars]}\]
 %
 The next example is defined using \keyw{fun} to escape the syntactic
-restrictions imposed on primitively recursive functions. The
-@{command datatype_compat} command is needed to register new-style datatypes
-for use with \keyw{fun} and \keyw{function}
-(Section~\ref{sssec:datatype-compat}):
+restrictions imposed on primitively recursive functions:
 *}
 
-    datatype_compat nat
-
-text {* \blankline *}
-
     fun at_least_two :: "nat \<Rightarrow> bool" where
       "at_least_two (Succ (Succ _)) \<longleftrightarrow> True" |
       "at_least_two _ \<longleftrightarrow> False"
@@ -3218,12 +3211,6 @@
 both views would make sense (for a different set of constructors).
 
 \item
-\emph{The \emph{\keyw{derive}} command from the \emph{Archive of Formal Proofs}
-has not yet been fully ported to the new-style datatypes.} Specimens featuring
-nested recursion require the use of @{command datatype_compat}
-(Section~\ref{sssec:datatype-compat}).
-
-\item
 \emph{The names of variables are often suboptimal in the properties generated by
 the package.}
 
@@ -3241,8 +3228,9 @@
 Kun\v{c}ar implemented the @{text transfer} and @{text lifting} plugins.
 Florian Haftmann and Christian Urban provided general advice on Isabelle and
 package writing. Stefan Milius and Lutz Schr\"oder found an elegant proof that
-eliminated one of the BNF proof obligations. Andreas Lochbihler, Tobias Nipkow,
-and Christian Sternagel suggested many textual improvements to this tutorial.
+eliminated one of the BNF proof obligations. Gerwin Klein, Andreas Lochbihler,
+Tobias Nipkow, and Christian Sternagel suggested many textual improvements to
+this tutorial.
 *}
 
 end