--- a/src/Doc/Tutorial/ToyList/ToyList.thy Mon Sep 01 16:17:46 2014 +0200 +++ b/src/Doc/Tutorial/ToyList/ToyList.thy Mon Sep 01 16:17:46 2014 +0200 @@ -1,5 +1,5 @@ theory ToyList -imports Datatype +imports Old_Datatype begin text{*\noindent