diff -r d6134fb5a49f -r da3e88ea6c72 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Sat Nov 21 17:35:55 2009 +0100
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Sat Nov 21 17:37:07 2009 +0100
@@ -552,7 +552,7 @@
 
 apply (simp only: wf_java_mdecl_def)
 apply (subgoal_tac "(\<forall>y\<in>set pns. y \<notin> set (map fst lvars))")
-apply (simp add: init_vars_def locvars_xstate_def locvars_locals_def galldefs unique_def split_def map_of_map_as_map_upd)
+apply (simp add: init_vars_def locvars_xstate_def locvars_locals_def galldefs unique_def split_def map_of_map_as_map_upd del: map_map)
 apply (intro strip)
 apply (simp (no_asm_simp) only: append_Cons [THEN sym])
 apply (rule progression_lvar_init_aux)