diff -r 9cb98d34f593 -r e88e980ed735 src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Sun Jan 15 14:55:30 2012 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Sun Jan 15 18:55:27 2012 +0100
@@ -95,7 +95,7 @@
 "(class G C = None) = (class (comp G) C = None)"
 apply (simp add: class_def comp_def compClass_def)
 apply (simp add: map_of_in_set)
-apply (simp add: image_compose [THEN sym] o_def split_beta del: image_compose)
+apply (simp add: image_compose [THEN sym] o_def split_beta)
 done
 
 lemma comp_is_class: "is_class (comp G) C = is_class G C"
@@ -170,7 +170,7 @@
 apply (simp only: image_compose [THEN sym])
 apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls).
   (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
-apply (simp del: image_compose)
+apply simp
 apply (simp add: fun_eq_iff split_beta)
 done
 
@@ -275,9 +275,9 @@
   = Option.map (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)"
 apply (induct xs)
 apply simp
-apply (simp del: split_paired_All)
+apply simp
 apply (case_tac "k = fst a")
-apply (simp del: split_paired_All)
+apply simp
 apply (subgoal_tac "(inv f (fst a, snd (f a))) = a", simp)
 apply (subgoal_tac "(fst a, snd (f a)) = f a", simp)
 apply (erule conjE)+
@@ -332,7 +332,7 @@
 defer
 
 apply (intro strip)
-apply (simp add: map_add_Some_iff map_of_map del: split_paired_Ex)
+apply (simp add: map_add_Some_iff map_of_map)
 apply (simp add: map_add_def)
 apply (subgoal_tac "inj (\<lambda>(s, m). (s, Ca, m))")
 apply (drule_tac g="(Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca))" and xs=ms