diff -r fcc9a30a7ef2 -r 16cc829b9c65 src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Thu Feb 28 18:11:11 2002 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Thu Feb 28 18:16:23 2002 +0100
@@ -13,9 +13,9 @@
 use_thy "JVM";
 use_thy "BVSpecTypeSafe";
 use_thy "BVExample";
+use_thy "LBVSpec"; 
 
 (* momentarily broken:
-use_thy "LBVSpec"; 
 use_thy "LBVCorrect";
 use_thy "LBVComplete";
 *)