# HG changeset patch
# User blanchet
# Date 1514925134 -3600
# Node ID 17fdb2c98083b36f76398669be5f5f97056e9c47
# Parent  79260409a6804190be37054cbda31ef27eb8eef1
removed para about 'old_datatype' in docs

diff -r 79260409a680 -r 17fdb2c98083 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Jan 02 20:38:41 2018 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Jan 02 21:32:14 2018 +0100
@@ -1216,17 +1216,6 @@
 @{text "[where \<dots>]"} attribute. The solution is to use the more robust
 @{text "[of \<dots>]"} syntax.
 \end{itemize}
-
-%FIXME old_datatype no longer exists
-The old command is still available as \keyw{old_datatype} in theory
-\<^file>\<open>~~/src/HOL/Library/Old_Datatype.thy\<close>. However, there is no general
-way to register old-style datatypes as new-style datatypes. If the objective
-is to define new-style datatypes with nested recursion through old-style
-datatypes, the old-style datatypes can be registered as a BNF
-(Section~\ref{sec:registering-bounded-natural-functors}). If the objective is
-to derive discriminators and selectors, this can be achieved using
-@{command free_constructors}
-(Section~\ref{sec:deriving-destructors-and-theorems-for-free-constructors}).
 \<close>