src/HOL/Library/Function_Algebras.thy

--- a/src/HOL/Library/Function_Algebras.thy	Thu Oct 31 16:54:22 2013 +0100
+++ b/src/HOL/Library/Function_Algebras.thy	Fri Nov 01 18:51:14 2013 +0100
@@ -83,10 +83,10 @@
 
 instance "fun" :: (type, group_add) group_add
   by default
-    (simp_all add: fun_eq_iff diff_minus)
+    (simp_all add: fun_eq_iff)
 
 instance "fun" :: (type, ab_group_add) ab_group_add
-  by default (simp_all add: diff_minus)
+  by default simp_all
 
 
 text {* Multiplicative structures *}