diff -r 106d62d106fc -r 25f1e89b5012 doc-src/TutorialI/Advanced/ROOT.ML
--- a/doc-src/TutorialI/Advanced/ROOT.ML	Tue Jan 08 18:08:02 2002 +0100
+++ b/doc-src/TutorialI/Advanced/ROOT.ML	Tue Jan 08 20:44:57 2002 +0100
@@ -1,4 +1,5 @@
 use "../settings.ML";
+no_document use_thy "While_Combinator";
 use_thy "simp";
 use_thy "WFrec";
 use_thy "Partial";