--- a/src/HOL/MicroJava/ROOT.ML Wed Mar 27 20:44:53 2002 +0100
+++ b/src/HOL/MicroJava/ROOT.ML Wed Mar 27 20:45:03 2002 +0100
@@ -14,7 +14,4 @@
use_thy "BVSpecTypeSafe";
use_thy "BVExample";
use_thy "LBVCorrect";
-
-(* momentarily broken:
use_thy "LBVComplete";
-*)