# HG changeset patch
# User wenzelm
# Date 1514921921 -3600
# Node ID 79260409a6804190be37054cbda31ef27eb8eef1
# Parent  4c94ec0488c7335e683396a0e579e3cff3ede11f
old_datatype no longer exists (cf. 706b1cf7b76d);

diff -r 4c94ec0488c7 -r 79260409a680 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Jan 02 19:52:36 2018 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Jan 02 20:38:41 2018 +0100
@@ -1217,6 +1217,7 @@
 @{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
diff -r 4c94ec0488c7 -r 79260409a680 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Tue Jan 02 19:52:36 2018 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Tue Jan 02 20:38:41 2018 +0100
@@ -712,13 +712,10 @@
 
 text \<open>
   \begin{matharray}{rcl}
-    @{command_def (HOL) "old_datatype"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{command_def (HOL) "old_rep_datatype"} & : & \<open>theory \<rightarrow> proof(prove)\<close> \\
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) old_datatype} (spec + @'and')
-    ;
     @@{command (HOL) old_rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
     ;
 
@@ -727,9 +724,6 @@
     cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
   \<close>}
 
-  \<^descr> @{command (HOL) "old_datatype"} defines old-style inductive
-  datatypes in HOL.
-
   \<^descr> @{command (HOL) "old_rep_datatype"} represents existing types as
   old-style datatypes.