diff -r 7b7051ae49a0 -r a47f51daa6dc src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Tue Jan 15 22:21:30 2002 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Tue Jan 15 22:22:05 2002 +0100
@@ -4,6 +4,10 @@
 add_path "JVM";
 add_path "BV";
 
+use_thy "JVMType"
+use_thy "JVMExceptions"
+
+(*
 use_thy "JTypeSafe";
 use_thy "Example";
 use_thy "JListExample";
@@ -11,6 +15,7 @@
 use_thy "BVSpecTypeSafe";
 use_thy "JVM";
 use_thy "LBVSpec"; 
+*)
 (* momentarily broken:
 use_thy "LBVCorrect";
 use_thy "LBVComplete";