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