diff -r 25a3531c0df5 -r b956bf0dc87c doc-src/IsarImplementation/Thy/ROOT.ML
--- a/doc-src/IsarImplementation/Thy/ROOT.ML	Thu Feb 26 20:57:59 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/ROOT.ML	Thu Feb 26 21:16:53 2009 +0100
@@ -1,8 +1,11 @@
-use_thy "Prelim";
-use_thy "Logic";
-use_thy "Tactic";
-use_thy "Proof";
-use_thy "Isar";
-use_thy "Local_Theory";
-use_thy "Integration";
-use_thy "ML";
+use_thys [
+  "Integration",
+  "Isar",
+  "Local_Theory",
+  "Logic",
+  "ML",
+  "Prelim",
+  "Proof",
+  "Syntax",
+  "Tactic"
+];