diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -113,7 +113,7 @@
 by (auto simp add: subcls1_def2 comp_classname comp_is_class)
 
 lemma comp_widen: "widen (comp G) = widen G"
-  apply (simp add: ext_iff)
+  apply (simp add: fun_eq_iff)
   apply (intro allI iffI)
   apply (erule widen.cases) 
   apply (simp_all add: comp_subcls1 widen.null)
@@ -122,7 +122,7 @@
   done
 
 lemma comp_cast: "cast (comp G) = cast G"
-  apply (simp add: ext_iff)
+  apply (simp add: fun_eq_iff)
   apply (intro allI iffI)
   apply (erule cast.cases) 
   apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
@@ -133,7 +133,7 @@
   done
 
 lemma comp_cast_ok: "cast_ok (comp G) = cast_ok G"
-  by (simp add: ext_iff cast_ok_def comp_widen)
+  by (simp add: fun_eq_iff cast_ok_def comp_widen)
 
 
 lemma compClass_fst [simp]: "(fst (compClass G C)) = (fst C)"
@@ -171,7 +171,7 @@
 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 add: ext_iff split_beta)
+apply (simp add: fun_eq_iff split_beta)
 done
 
 
@@ -322,7 +322,7 @@
   = (\<lambda>x. (fst x, Object, fst (snd x),
                         snd (snd (compMethod G Object (S, snd x)))))")
 apply (simp only:)
-apply (simp add: ext_iff)
+apply (simp add: fun_eq_iff)
 apply (intro strip)
 apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Object, m)) (S, Object, snd x)) = (S, snd x)")
 apply (simp only:)