diff -r d6134fb5a49f -r da3e88ea6c72 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sat Nov 21 17:35:55 2009 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sat Nov 21 17:37:07 2009 +0100
@@ -132,7 +132,7 @@
 apply (case_tac "vname = This")
 apply (simp add: inited_LT_def)
 apply (simp add: inited_LT_def)
-apply (simp (no_asm_simp) only: map_compose map_append [THEN sym] map.simps [THEN sym])
+apply (simp (no_asm_simp) only: map_map [symmetric] map_append [symmetric] map.simps [symmetric])
 apply (subgoal_tac "length (takeWhile (\<lambda>z. z \<noteq> vname) (pns @ map fst lvars)) < length (pTs @ map snd lvars)")
 apply (simp (no_asm_simp) only: List.nth_map ok_val.simps)
 apply (subgoal_tac "map_of lvars = map_of (map (\<lambda> p. (fst p, snd p)) lvars)")
@@ -166,7 +166,7 @@
 lemma inited_LT_at_index_no_err: " i < length (inited_LT C pTs lvars)
   \<Longrightarrow> inited_LT C pTs lvars ! i \<noteq> Err"
 apply (simp only: inited_LT_def)
-apply (simp only: map_compose map_append [THEN sym] map.simps [THEN sym] length_map)
+apply (simp only: map_map [symmetric] map_append [symmetric] map.simps [symmetric] length_map)
 apply (simp only: nth_map)
 apply simp
 done