diff -r 6d4ea2efa64b -r 0e4bb86c74fd doc-src/TutorialI/ROOT.ML
--- a/doc-src/TutorialI/ROOT.ML	Thu Jul 26 17:17:53 2012 +0200
+++ b/doc-src/TutorialI/ROOT.ML	Thu Jul 26 17:32:28 2012 +0200
@@ -27,14 +27,6 @@
 use_thy "Inductive/AB";
 use_thy "Inductive/Advanced";
 
-no_document use_thy "Types/Setup";
-use_thy "Types/Numbers";
-use_thy "Types/Pairs";
-use_thy "Types/Records";
-use_thy "Types/Typedefs";
-use_thy "Types/Overloading";
-use_thy "Types/Axioms";
-
 use_thy "Misc/Tree";
 use_thy "Misc/Tree2";
 use_thy "Misc/Plus";
@@ -53,6 +45,18 @@
 
 Thy_Output.indent_default := 0;
 
+use_thy "Protocol/NS_Public";
+
+use_thy "Documents/Documents";
+
+no_document use_thy "Types/Setup";
+use_thy "Types/Numbers";
+use_thy "Types/Pairs";
+use_thy "Types/Records";
+use_thy "Types/Typedefs";
+use_thy "Types/Overloading";
+use_thy "Types/Axioms";
+
 use_thy "Rules/Basic";
 use_thy "Rules/Blast";
 use_thy "Rules/Force";
@@ -65,6 +69,3 @@
 use_thy "Sets/Relations";
 use_thy "Sets/Recur";
 
-use_thy "Protocol/NS_Public";
-
-use_thy "Documents/Documents";