diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -521,7 +521,7 @@
 apply (case_tac lvals) apply simp
 apply (simp (no_asm_simp) )
 
-apply (rule_tac ?lvars1.0 = "(prfx @ [default_val (snd a)]) @ lista" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?lvars1.0 = "(prfx @ [default_val (snd a)]) @ list" in progression_transitive, rule HOL.refl)
 apply (case_tac a) apply (simp (no_asm_simp) add: compInit_def)
 apply (rule_tac ?instrs0.0 = "[load_default_val b]" in progression_transitive, simp)
 apply (rule progression_one_step)