--- a/src/HOL/MicroJava/Comp/CorrComp.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy Tue Oct 07 16:07:50 2008 +0200
@@ -1138,7 +1138,7 @@
apply (rule_tac ?instrs0.0 = "(compInitLvars (pns, lvars, blk, res) lvars)" in progression_transitive, rule HOL.refl)
apply (rule_tac C=md in progression_lvar_init, assumption, assumption, assumption)
apply (simp (no_asm_simp)) (* length pns = length pvs *)
-apply (simp (no_asm_simp)) (* length lvars = length (replicate (length lvars) arbitrary) *)
+apply (simp (no_asm_simp)) (* length lvars = length (replicate (length lvars) undefined) *)
(* body statement *)