src/HOL/MicroJava/Comp/LemmasComp.thy

       with as show "fst a \<in> fst ` set list" by (simp add: fst_a_x)
     qed
 
     with fst_eq Cons 
     show "unique (map f (a # list)) = unique (a # list)"
-      by (simp add: unique_def fst_set)
+      by (simp add: unique_def fst_set image_compose)
   qed
 qed
 
 lemma comp_unique: "unique (comp G) = unique G"
 apply (simp add: comp_def)

   Option.map (\<lambda> (D,rT,b).  (D, rT, mtd_mb (compMethod G D (S, rT, b))))
              (method (G, C) S))"
 apply (simp add: method_def)
 apply (frule wf_subcls1)
 apply (simp add: comp_class_rec)
-apply (simp add: map_compose [THEN sym] split_iter split_compose del: map_compose)
+apply (simp add: split_iter split_compose map_map[symmetric] del: map_map)
 apply (rule_tac R="%x y. ((x S) = (Option.map (\<lambda>(D, rT, b). 
   (D, rT, snd (snd (compMethod G D (S, rT, b))))) (y S)))" 
   in class_rec_relation)
 apply assumption
 

 defer                           (* inj \<dots> *)
 apply (simp add: inj_on_def split_beta) 
 apply (simp add: split_beta compMethod_def)
 apply (simp add: map_of_map [THEN sym])
 apply (simp add: split_beta)
-apply (simp add: map_compose [THEN sym] Fun.comp_def split_beta)
+apply (simp add: Fun.comp_def split_beta)
 apply (subgoal_tac "(\<lambda>x\<Colon>(vname list \<times> fdecl list \<times> stmt \<times> expr) mdecl.
                     (fst x, Object,
                      snd (compMethod G Object
                            (inv (\<lambda>(s\<Colon>sig, m\<Colon>ty \<times> vname list \<times> fdecl list \<times> stmt \<times> expr).
                                     (s, Object, m))