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