diff -r b1ebe0320d79 -r 69971d68fe03 src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Sun Dec 16 00:20:17 2001 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Mon Dec 17 13:25:18 2001 +0100
@@ -7,7 +7,7 @@
 use_thy "JTypeSafe";
 use_thy "Example";
 use_thy "JListExample";
-(* use_thy "JVMListExample"; *)
+use_thy "JVMListExample";
 use_thy "BVSpecTypeSafe";
 use_thy "JVM";
 use_thy "LBVSpec";