--- a/src/HOL/Tools/group_cancel.ML Thu Oct 31 16:54:22 2013 +0100
+++ b/src/HOL/Tools/group_cancel.ML Fri Nov 01 18:51:14 2013 +0100
@@ -25,7 +25,7 @@
val sub1 = @{lemma "(A::'a::ab_group_add) == k + a ==> A - b == k + (a - b)"
by (simp only: add_diff_eq)}
val sub2 = @{lemma "(B::'a::ab_group_add) == k + b ==> a - B == - k + (a - b)"
- by (simp only: diff_minus minus_add add_ac)}
+ by (simp only: minus_add diff_conv_add_uminus add_ac)}
val neg1 = @{lemma "(A::'a::ab_group_add) == k + a ==> - A == - k + - a"
by (simp only: minus_add_distrib)}
val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"