--- a/doc-src/TutorialI/Fun/ROOT.ML Wed Aug 11 11:56:57 2010 +0200 +++ b/doc-src/TutorialI/Fun/ROOT.ML Wed Aug 11 12:03:57 2010 +0200 @@ -1,2 +1,2 @@ -use "../settings"; +use "../settings.ML"; use_thy "fun0";