diff -r e4d58f1be05b -r 4cae97480a6d src/HOL/MicroJava/BV/StepMono.thy
--- a/src/HOL/MicroJava/BV/StepMono.thy	Sat Aug 19 12:49:19 2000 +0200
+++ b/src/HOL/MicroJava/BV/StepMono.thy	Sun Aug 20 17:45:20 2000 +0200
@@ -15,7 +15,7 @@
 
 lemma sup_loc_some [rulify]:
 "\<forall> y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = Some t \<longrightarrow> (\<exists>t. b!n = Some t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
-proof (induct "?P" b)
+proof (induct (open) ?P b)
   show "?P []" by simp
 
   case Cons
@@ -59,7 +59,7 @@
 
 lemma append_length_n [rulify]: 
 "\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
-proof (induct "?P" "x")
+proof (induct (open) ?P x)
   show "?P []" by simp
 
   fix l ls assume Cons: "?P ls"
@@ -122,7 +122,7 @@
   assume app: "app (i, G, rT, s1)"
   
   show ?thesis
-  proof (cases i)
+  proof (cases (open) i)
     case Load
     
     from G
@@ -308,7 +308,7 @@
     by (auto dest!: app_step_some);
 
   have "G \<turnstile> (a1',b1') <=s (a2',b2')"
-  proof (cases i)
+  proof (cases (open) i)
     case Load
 
     with s app1