diff -r 92cd56dfc17e -r 8e4307d1207a doc-src/TutorialI/Misc/ROOT.ML
--- a/doc-src/TutorialI/Misc/ROOT.ML	Wed Nov 29 18:42:40 2000 +0100
+++ b/doc-src/TutorialI/Misc/ROOT.ML	Thu Nov 30 13:56:46 2000 +0100
@@ -5,6 +5,7 @@
 use_thy "fakenat";
 use_thy "natsum";
 use_thy "pairs";
+use_thy "Option2";
 use_thy "types";
 use_thy "prime_def";
 use_thy "simp";