diff -r e4d58f1be05b -r 4cae97480a6d src/HOL/MicroJava/BV/Convert.thy
--- a/src/HOL/MicroJava/BV/Convert.thy	Sat Aug 19 12:49:19 2000 +0200
+++ b/src/HOL/MicroJava/BV/Convert.thy	Sun Aug 20 17:45:20 2000 +0200
@@ -241,7 +241,7 @@
     { 
       fix b
       have "?Q (l#ls) b"
-      proof (cases b)
+      proof (cases (open) b)
         case Nil
         thus ?thesis by (auto dest: sup_loc_length)
       next