old_datatype no longer exists (cf. 706b1cf7b76d);
--- 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
--- 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.