added .ML extension

--- 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";