diff -r a6ce43a59d4a -r 06cce9be31a4 src/HOL/MicroJava/BV/Correct.thy --- a/src/HOL/MicroJava/BV/Correct.thy Sat Oct 26 13:05:27 2002 +0200 +++ b/src/HOL/MicroJava/BV/Correct.thy Sun Oct 27 23:34:02 2002 +0100 @@ -334,8 +334,7 @@ "\rT C sig. hp x = None \ correct_frames G hp phi rT sig frs \ - G,hp \ obj \ - \ correct_frames G (hp(x \ obj)) phi rT sig frs" + correct_frames G (hp(x \ obj)) phi rT sig frs" apply (induct frs) apply simp apply clarify