diff -r 8b9e5d776ef3 -r 373727835757 src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Mon Jul 30 19:22:27 2007 +0200
+++ b/src/HOL/MicroJava/ROOT.ML	Mon Jul 30 19:46:13 2007 +0200
@@ -1,20 +1,8 @@
-goals_limit := 1;
-
-add_path "J";
-add_path "JVM";
-add_path "BV";
-add_path "Comp";
+(* $Id$ *)
 
 no_document use_thy "While_Combinator";
 
-use_thy "JTypeSafe";
-use_thy "Example";
-use_thy "JListExample";
-use_thy "JVMListExample";
-use_thy "JVMDefensive";
-use_thy "LBVJVM";
-use_thy "BVNoTypeError";
-use_thy "BVExample";
-
-use_thy "CorrComp";
-use_thy "CorrCompTp";
+use_thys ["J/JTypeSafe", "J/Example", "J/JListExample",
+  "JVM/JVMListExample", "JVM/JVMDefensive", "BV/LBVJVM",
+  "BV/BVNoTypeError", "BV/BVExample", "Comp/CorrComp",
+  "Comp/CorrCompTp"];