1.1 --- a/src/HOL/MicroJava/BV/Correct.thy	Thu Dec 07 16:21:47 2000 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Dec 07 16:22:39 2000 +0100
     1.3 @@ -39,9 +39,9 @@
     1.4  "correct_frames G hp phi rT0 sig0 (f#frs) =
     1.5  	(let (stk,loc,C,sig,pc) = f in
     1.6    (\<exists>ST LT rT maxs maxl ins.
     1.7 -    phi C sig ! pc = Some (ST,LT) \<and> 
     1.8 +    phi C sig ! pc = Some (ST,LT) \<and> is_class G C \<and> 
     1.9      method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \<and>
    1.10 -	(\<exists>C' mn pTs k. pc = k+1 \<and> ins!k = (Invoke C' mn pTs) \<and>
    1.11 +	(\<exists>C' mn pTs k. pc = k+1 \<and> ins!k = (Invoke C' mn pTs) \<and> 
    1.12           (mn,pTs) = sig0 \<and> 
    1.13           (\<exists>apTs D ST' LT'.
    1.14           (phi C sig)!k = Some ((rev apTs) @ (Class D) # ST', LT') \<and>
    1.15 @@ -64,6 +64,7 @@
    1.16  			(let (stk,loc,C,sig,pc) = f
    1.17  		         in
    1.18                           \<exists>rT maxs maxl ins s.
    1.19 +                         is_class G C \<and>
    1.20                           method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \<and>
    1.21                           phi C sig ! pc = Some s \<and>
    1.22  			 correct_frame G hp s maxl ins f \<and>