Updated.

--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed May 07 10:59:53 2008 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Wed May 07 10:59:54 2008 +0200
@@ -9,7 +9,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ ToyList\isanewline
-\isakeyword{imports}\ PreList\isanewline
+\isakeyword{imports}\ Datatype\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%
@@ -23,7 +23,7 @@
 HOL already has a predefined theory of lists called \isa{List} ---
 \isa{ToyList} is merely a small fragment of it chosen as an example. In
 contrast to what is recommended in \S\ref{sec:Basic:Theories},
-\isa{ToyList} is not based on \isa{Main} but on \isa{PreList}, a
+\isa{ToyList} is not based on \isa{Main} but on \isa{Datatype}, a
 theory that contains pretty much everything but lists, thus avoiding
 ambiguities caused by defining lists twice.%
 \end{isamarkuptext}%