diff -r dceea9dbdedd -r b85acd66f715 doc-src/TutorialI/Misc/ROOT.ML
--- a/doc-src/TutorialI/Misc/ROOT.ML	Fri Dec 21 17:31:45 2001 +0100
+++ b/doc-src/TutorialI/Misc/ROOT.ML	Fri Dec 21 19:55:39 2001 +0100
@@ -8,7 +8,6 @@
 use_thy "Option2";
 use_thy "types";
 use_thy "prime_def";
-use_thy "Translations";
 use_thy "simp";
 use_thy "Itrev";
 use_thy "AdvancedInd";