src/HOL/MicroJava/Comp/CorrComp.thy

 apply (clarsimp, rule progression_refl)
 apply (intro strip)
 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)
 apply (simp (no_asm_simp) add: load_default_val_def)
 apply (rule conjI, simp)+ apply (rule HOL.refl)