diff -r eb94cfaaf5d4 -r 66b189dc5b83 doc-src/HOL/HOL.tex
--- a/doc-src/HOL/HOL.tex	Wed May 25 22:21:38 2011 +0200
+++ b/doc-src/HOL/HOL.tex	Thu May 26 13:37:11 2011 +0200
@@ -1249,9 +1249,7 @@
 shown.  The constructions are fairly standard and can be found in the
 respective theory files. Although the sum and product types are
 constructed manually for foundational reasons, they are represented as
-actual datatypes later (see {\S}\ref{subsec:datatype:rep_datatype}).
-Therefore, the theory \texttt{Datatype} should be used instead of
-\texttt{Sum} or \texttt{Prod}.
+actual datatypes later.
 
 \begin{figure}
 \begin{constants}
@@ -1375,7 +1373,7 @@
 the order of the two cases.
 Both \texttt{primrec} and \texttt{case} are realized by a recursion operator
 \cdx{nat_rec}, which is available because \textit{nat} is represented as
-a datatype (see {\S}\ref{subsec:datatype:rep_datatype}).
+a datatype.
 
 %The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
 %Recursion along this relation resembles primitive recursion, but is
@@ -1940,32 +1938,6 @@
 and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.
 
 
-\subsection{Representing existing types as datatypes}\label{subsec:datatype:rep_datatype}
-
-For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt
-  +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section,
-but by more primitive means using \texttt{typedef}. To be able to use the
-tactics \texttt{induct_tac} and \texttt{case_tac} and to define functions by
-primitive recursion on these types, such types may be represented as actual
-datatypes.  This is done by specifying the constructors of the desired type,
-plus a proof of the  induction rule, as well as theorems
-stating the distinctness and injectivity of constructors in a {\tt
-rep_datatype} section.  For the sum type this works as follows:
-\begin{ttbox}
-rep_datatype (sum) Inl Inr
-proof -
-  fix P
-  fix s :: "'a + 'b"
-  assume x: "!!x::'a. P (Inl x)" and y: "!!y::'b. P (Inr y)"
-  then show "P s" by (auto intro: sumE [of s])
-qed simp_all
-\end{ttbox}
-The datatype package automatically derives additional theorems for recursion
-and case combinators from these rules.  Any of the basic HOL types mentioned
-above are represented as datatypes.  Try an induction on \texttt{bool}
-today.
-
-
 \subsection{Examples}
 
 \subsubsection{The datatype $\alpha~mylist$}