diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Fset.thy
--- a/src/HOL/Library/Fset.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Library/Fset.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -51,7 +51,7 @@
 lemma member_code [code]:
   "member (Set xs) = List.member xs"
   "member (Coset xs) = Not \<circ> List.member xs"
-  by (simp_all add: ext_iff member_def fun_Compl_def bool_Compl_def)
+  by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def)
 
 lemma member_image_UNIV [simp]:
   "member ` UNIV = UNIV"
@@ -252,13 +252,13 @@
   show "inf A (Set xs) = Set (List.filter (member A) xs)"
     by (simp add: inter project_def Set_def)
   have *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member)"
-    by (simp add: ext_iff)
+    by (simp add: fun_eq_iff)
   have "member \<circ> fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs =
     fold More_Set.remove xs \<circ> member"
-    by (rule fold_apply) (simp add: ext_iff)
+    by (rule fold_apply) (simp add: fun_eq_iff)
   then have "fold More_Set.remove xs (member A) = 
     member (fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs A)"
-    by (simp add: ext_iff)
+    by (simp add: fun_eq_iff)
   then have "inf A (Coset xs) = fold remove xs A"
     by (simp add: Diff_eq [symmetric] minus_set *)
   moreover have "\<And>x y :: 'a. Fset.remove y \<circ> Fset.remove x = Fset.remove x \<circ> Fset.remove y"
@@ -277,13 +277,13 @@
   "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
 proof -
   have *: "\<And>x::'a. insert = (\<lambda>x. Fset \<circ> Set.insert x \<circ> member)"
-    by (simp add: ext_iff)
+    by (simp add: fun_eq_iff)
   have "member \<circ> fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs =
     fold Set.insert xs \<circ> member"
-    by (rule fold_apply) (simp add: ext_iff)
+    by (rule fold_apply) (simp add: fun_eq_iff)
   then have "fold Set.insert xs (member A) =
     member (fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs A)"
-    by (simp add: ext_iff)
+    by (simp add: fun_eq_iff)
   then have "sup (Set xs) A = fold insert xs A"
     by (simp add: union_set *)
   moreover have "\<And>x y :: 'a. Fset.insert y \<circ> Fset.insert x = Fset.insert x \<circ> Fset.insert y"