src/HOL/NSA/NSComplex.thy

--- a/src/HOL/NSA/NSComplex.thy	Fri Dec 18 18:48:27 2009 -0800
+++ b/src/HOL/NSA/NSComplex.thy	Fri Dec 18 19:00:11 2009 -0800
@@ -161,7 +161,7 @@
 
 lemma hcomplex_add_minus_eq_minus:
       "x + y = (0::hcomplex) ==> x = -y"
-apply (drule OrderedGroup.equals_zero_I)
+apply (drule OrderedGroup.minus_unique)
 apply (simp add: minus_equation_iff [of x y])
 done