diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Library/More_Set.thy
--- a/src/HOL/Library/More_Set.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Library/More_Set.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -18,7 +18,7 @@
 lemma fun_left_comm_idem_remove:
   "fun_left_comm_idem remove"
 proof -
-  have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: ext_iff remove_def)
+  have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
   show ?thesis by (simp only: fun_left_comm_idem_remove rem)
 qed
 
@@ -26,7 +26,7 @@
   assumes "finite A"
   shows "B - A = Finite_Set.fold remove B A"
 proof -
-  have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: ext_iff remove_def)
+  have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def)
   show ?thesis by (simp only: rem assms minus_fold_remove)
 qed
 
@@ -124,6 +124,6 @@
 
 lemma not_set_compl:
   "Not \<circ> set xs = - set xs"
-  by (simp add: fun_Compl_def bool_Compl_def comp_def ext_iff)
+  by (simp add: fun_Compl_def bool_Compl_def comp_def fun_eq_iff)
 
 end