diff -r cae0f68b693b -r db3e412c4cb1 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Fri Oct 19 16:20:27 2007 +0200
+++ b/src/HOL/OrderedGroup.thy	Fri Oct 19 19:45:29 2007 +0200
@@ -879,7 +879,7 @@
   then have "a + a + - a = - a" by simp
   then have "a + (a + - a) = - a" by (simp only: add_assoc)
   then have a: "- a = a" by simp (*FIXME tune proof*)
-  show "a = 0" apply rule
+  show "a = 0" apply (rule antisym)
   apply (unfold neg_le_iff_le [symmetric, of a])
   unfolding a apply simp
   unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a]