--- a/src/Doc/Tutorial/ToyList/ToyList.thy Thu Sep 18 16:47:40 2014 +0200
+++ b/src/Doc/Tutorial/ToyList/ToyList.thy Thu Sep 18 16:47:40 2014 +0200
@@ -1,14 +1,14 @@
theory ToyList
-imports Old_Datatype
+imports BNF_Least_Fixpoint
begin
text{*\noindent
HOL already has a predefined theory of lists called @{text List} ---
@{text ToyList} is merely a small fragment of it chosen as an example. In
contrast to what is recommended in \S\ref{sec:Basic:Theories},
-@{text ToyList} is not based on @{text Main} but on @{text Datatype}, a
-theory that contains pretty much everything but lists, thus avoiding
-ambiguities caused by defining lists twice.
+@{text ToyList} is not based on @{text Main} but on
+@{text BNF_Least_Fixpoint}, a theory that contains pretty much everything
+but lists, thus avoiding ambiguities caused by defining lists twice.
*}
datatype 'a list = Nil ("[]")