diff -r 749fd046002f -r 0a9d14823644 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Thu Feb 22 11:47:35 2001 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Feb 22 18:03:11 2001 +0100
@@ -25,11 +25,6 @@
                          approx_stk G hp stk ST  \<and> approx_loc G hp loc LT \<and> 
                          pc < length ins \<and> length loc=length(snd sig)+maxl+1"
 
-  correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] 
-                        => frame => bool"
-  "correct_frame_opt G hp s == 
-    case s of None => \<lambda>maxl ins f. False | Some t => correct_frame G hp t"
-
 
 consts
  correct_frames  :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] => bool"