--- a/src/HOL/MicroJava/BV/Correct.ML Thu Dec 02 09:09:30 1999 +0100
+++ b/src/HOL/MicroJava/BV/Correct.ML Mon Dec 06 14:23:45 1999 +0100
@@ -17,7 +17,7 @@
Goalw [hext_def]
-"hp a = Some (cn,od') \\<longrightarrow> hp \\<le>| (hp(a \\<mapsto> (cn,od)))";
+"hp a = Some (C,od') \\<longrightarrow> hp \\<le>| (hp(a \\<mapsto> (C,od)))";
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed_spec_mp "sup_heap_update_value";
@@ -254,9 +254,9 @@
Delsimps [fun_upd_apply];
Goal
"\\<forall>rT C sig. correct_frames G hp phi rT sig frs \\<longrightarrow> \
-\ hp a = Some (cn,od) \\<longrightarrow> map_of (fields (G, cn)) fl = Some fd \\<longrightarrow> \
+\ hp a = Some (C,od) \\<longrightarrow> map_of (fields (G, C)) fl = Some fd \\<longrightarrow> \
\ G,hp\\<turnstile>v\\<Colon>\\<preceq>fd \
-\ \\<longrightarrow> correct_frames G (hp(a \\<mapsto> (cn, od(fl\\<mapsto>v)))) phi rT sig frs";
+\ \\<longrightarrow> correct_frames G (hp(a \\<mapsto> (C, od(fl\\<mapsto>v)))) phi rT sig frs";
by (induct_tac "frs" 1);
by (Asm_full_simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [split_def,correct_frame_def]) 1);