--- a/src/HOL/Library/Function_Algebras.thy Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Library/Function_Algebras.thy Tue Sep 07 10:05:19 2010 +0200
@@ -57,7 +57,7 @@
qed (simp add: plus_fun_def add.assoc)
instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof
-qed (simp_all add: plus_fun_def expand_fun_eq)
+qed (simp_all add: plus_fun_def ext_iff)
instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof
qed (simp add: plus_fun_def add.commute)
@@ -106,7 +106,7 @@
qed (simp_all add: zero_fun_def times_fun_def)
instance "fun" :: (type, zero_neq_one) zero_neq_one proof
-qed (simp add: zero_fun_def one_fun_def expand_fun_eq)
+qed (simp add: zero_fun_def one_fun_def ext_iff)
text {* Ring structures *}