diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Set_Algebras.thy
--- a/src/HOL/Library/Set_Algebras.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Library/Set_Algebras.thy	Tue Sep 07 10:05:19 2010 +0200
@@ -72,7 +72,7 @@
   show "monoid_add.listsum set_plus {0::'a} = listsum_set"
     by (simp only: listsum_set_def)
   show "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
-    by (simp add: set_add.setsum_def setsum_set_def expand_fun_eq)
+    by (simp add: set_add.setsum_def setsum_set_def ext_iff)
 qed
 
 interpretation set_mult!: semigroup "set_times :: 'a::semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
@@ -117,7 +117,7 @@
   show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
     by (simp add: power_set_def)
   show "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
-    by (simp add: set_mult.setprod_def setprod_set_def expand_fun_eq)
+    by (simp add: set_mult.setprod_def setprod_set_def ext_iff)
 qed
 
 lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"