--- a/src/HOL/MicroJava/BV/Correct.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Sat Nov 01 14:20:38 2014 +0100
@@ -299,7 +299,7 @@
hp a = Some (C,fs) \<longrightarrow>
map_of (fields (G, C)) fl = Some fd \<longrightarrow>
G,hp\<turnstile>v::\<preceq>fd
- \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, fs(fl\<mapsto>v)))) phi rT sig frs";
+ \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, fs(fl\<mapsto>v)))) phi rT sig frs"
apply (induct frs)
apply simp
apply clarify