diff -r f00857c7539b -r 1275417e3930 doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Mon Aug 16 19:06:59 2004 +0200
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Mon Aug 16 19:47:01 2004 +0200
@@ -1,4 +1,6 @@
-theory ToyList = PreList:
+theory ToyList
+import PreList
+begin
 
 text{*\noindent
 HOL already has a predefined theory of lists called @{text"List"} ---