--- a/doc-src/TutorialI/ToyList/ROOT.ML Mon Sep 04 21:20:14 2000 +0200 +++ b/doc-src/TutorialI/ToyList/ROOT.ML Tue Sep 05 09:03:17 2000 +0200 @@ -1,2 +1,3 @@ +use "../settings.ML"; use_thy "ToyList";