--- a/src/Doc/Tutorial/ToyList/ToyList1.txt	Fri Nov 07 15:19:30 2014 +0100
+++ b/src/Doc/Tutorial/ToyList/ToyList1.txt	Fri Nov 07 16:13:05 2014 +0100
@@ -1,7 +1,11 @@
 theory ToyList
-imports BNF_Least_Fixpoint
+imports Main
 begin
 
+no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65)
+hide_type list
+hide_const rev
+
 datatype 'a list = Nil                          ("[]")
                  | Cons 'a "'a list"            (infixr "#" 65)