diff -r 296b03b79505 -r 816f566c414f src/HOL/MicroJava/BV/Correct.ML
--- a/src/HOL/MicroJava/BV/Correct.ML	Wed Dec 01 11:20:24 1999 +0100
+++ b/src/HOL/MicroJava/BV/Correct.ML	Wed Dec 01 18:22:28 1999 +0100
@@ -253,10 +253,10 @@
 
 Delsimps [fun_upd_apply]; 
 Goal
-"\\<forall>rT C ml. correct_frames G hp phi rT C ml frs \\<longrightarrow> \
+"\\<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> \
 \    G,hp\\<turnstile>v\\<Colon>\\<preceq>fd \
-\ \\<longrightarrow> correct_frames G (hp(a \\<mapsto> (cn, od(fl\\<mapsto>v)))) phi rT C ml frs";
+\ \\<longrightarrow> correct_frames G (hp(a \\<mapsto> (cn, 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);
@@ -267,9 +267,9 @@
 
 
 Goal
-"\\<forall>rT C ml. hp x = None \\<longrightarrow> correct_frames G hp phi rT C ml frs \\<and> \
+"\\<forall>rT C sig. hp x = None \\<longrightarrow> correct_frames G hp phi rT sig frs \\<and> \
 \    oconf G hp obj \
-\ \\<longrightarrow> correct_frames G (hp(newref hp \\<mapsto> obj)) phi rT C ml frs";
+\ \\<longrightarrow> correct_frames G (hp(newref hp \\<mapsto> obj)) phi rT sig frs";
 by (induct_tac "frs" 1);
 by  (asm_full_simp_tac (simpset() addsimps []) 1);
 by (asm_full_simp_tac (simpset() addsimps [split_def,correct_frame_def]) 1);