1.1 --- a/src/HOL/MicroJava/BV/Correct.thy	Thu Feb 22 11:47:35 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Feb 22 18:03:11 2001 +0100
     1.3 @@ -25,11 +25,6 @@
     1.4                           approx_stk G hp stk ST  \<and> approx_loc G hp loc LT \<and> 
     1.5                           pc < length ins \<and> length loc=length(snd sig)+maxl+1"
     1.6  
     1.7 -  correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] 
     1.8 -                        => frame => bool"
     1.9 -  "correct_frame_opt G hp s == 
    1.10 -    case s of None => \<lambda>maxl ins f. False | Some t => correct_frame G hp t"
    1.11 -
    1.12  
    1.13  consts
    1.14   correct_frames  :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] => bool"