diff -r 2d9cf954a829 -r cce82e360c2f src/HOL/Library/Function_Algebras.thy
--- a/src/HOL/Library/Function_Algebras.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Library/Function_Algebras.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -71,7 +71,7 @@
   by default (simp add: fun_eq_iff add.commute)
 
 instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
-  by default simp
+  by default (simp_all add: fun_eq_iff diff_diff_eq)
 
 instance "fun" :: (type, monoid_add) monoid_add
   by default (simp_all add: fun_eq_iff)