--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Thu Oct 24 12:07:31 2002 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Thu Oct 24 12:08:33 2002 +0200
@@ -281,7 +281,7 @@
by (clarsimp simp add: app_def)
with eff stk loc pc'
- have "check_instr (ins!pc) G hp stk loc C sig pc (length ins) frs'"
+ have "check_instr (ins!pc) G hp stk loc C sig pc frs'"
proof (cases "ins!pc")
case (Getfield F C)
with app stk loc phi obtain v vT stk' where
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Thu Oct 24 12:07:31 2002 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Thu Oct 24 12:08:33 2002 +0200
@@ -668,7 +668,7 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs2 map_eq_Cons wt_jvm_prog_def
+apply (clarsimp simp add: defs2 map_eq_Cons wt_jvm_prog_def split_beta
split: option.split split_if_asm)
apply (frule conf_widen)
apply assumption+