diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -116,7 +116,7 @@
 apply (clarify)
 apply (drule_tac x=kr in spec)
 apply (simp only: rev.simps)
-apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev list @ [a])) = empty (rev kr[\<mapsto>]rev list)([k'][\<mapsto>][a])")
+apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])")
 apply (simp only:)
 apply (case_tac "k' = k")
 apply simp
@@ -1531,9 +1531,9 @@
 apply (induct m)
 apply simp
 apply (intro strip)
-apply (subgoal_tac "na \<le> n \<or> na = Suc n")
+apply (subgoal_tac "n \<le> m \<or> n = Suc m")
 apply (erule disjE)
-apply (frule_tac x=na in spec, drule_tac x=xs in spec, drule mp, assumption)
+apply (frule_tac x=n in spec, drule_tac x=xs in spec, drule mp, assumption)
 apply (rule set_drop_Suc [THEN subset_trans], assumption)
 apply auto
 done
@@ -2310,7 +2310,7 @@
 apply (drule_tac x="lvars_pre @ [a]" in spec)
 apply (drule_tac x="lvars0" in spec)
 apply (simp (no_asm_simp) add: compInitLvars_def)
-apply (rule_tac ?bc1.0="compInit jmb a" and ?bc2.0="compInitLvars jmb list"
+apply (rule_tac ?bc1.0="compInit jmb a" and ?bc2.0="compInitLvars jmb lvars"
   in bc_mt_corresp_comb)
 apply (simp (no_asm_simp) add: compInitLvars_def)+