--- a/src/HOL/MicroJava/BV/Step.thy Sat Aug 19 12:49:19 2000 +0200
+++ b/src/HOL/MicroJava/BV/Step.thy Sun Aug 20 17:45:20 2000 +0200
@@ -187,7 +187,7 @@
lemma appIAdd[simp]:
"app (IAdd, G, rT, s) = (\<exists> ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))" (is "?app s = ?P s")
-proof (cases s)
+proof (cases (open) s)
case Pair
have "?app (a,b) = ?P (a,b)"
proof (cases "a")
@@ -234,7 +234,7 @@
G \<turnstile> X \<preceq> Class C \<and>
(\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and>
method (G,C) (mn,fpTs) \<noteq> None)" (is "?app s = ?P s")
-proof (cases s)
+proof (cases (open) s)
case Pair
have "?app (a,b) \<Longrightarrow> ?P (a,b)"
proof -