# HG changeset patch
# User kleing
# Date 1011254470 -3600
# Node ID d655138ddadf5a35075ede534792dca3413299ab
# Parent  27debaf2112da953e476427f95aa16d48f4d4ee2
fixed

diff -r 27debaf2112d -r d655138ddadf 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";