src/HOL/MicroJava/ROOT.ML

--- a/src/HOL/MicroJava/ROOT.ML	Wed Jan 16 23:19:34 2002 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Thu Jan 17 09:01:10 2002 +0100
@@ -4,10 +4,6 @@
 add_path "JVM";
 add_path "BV";
 
-use_thy "JVMType"
-use_thy "JVMExceptions"
-
-(*
 use_thy "JTypeSafe";
 use_thy "Example";
 use_thy "JListExample";
@@ -15,7 +11,7 @@
 use_thy "BVSpecTypeSafe";
 use_thy "JVM";
 use_thy "LBVSpec"; 
-*)
+
 (* momentarily broken:
 use_thy "LBVCorrect";
 use_thy "LBVComplete";