--- a/src/HOL/MicroJava/Comp/LemmasComp.thy Sat Nov 21 17:35:55 2009 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Sat Nov 21 17:37:07 2009 +0100
@@ -68,7 +68,7 @@
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
@@ -292,7 +292,7 @@
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)
@@ -311,7 +311,7 @@
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