src/HOL/Complex/NSComplex.thy

--- a/src/HOL/Complex/NSComplex.thy	Thu Dec 25 23:18:04 2003 +0100
+++ b/src/HOL/Complex/NSComplex.thy	Sat Dec 27 21:02:14 2003 +0100
@@ -1015,7 +1015,7 @@
 
 lemma hcmod_triangle_ineq2: "hcmod(b + a) - hcmod b <= hcmod a"
 apply (cut_tac x1 = "b" and y1 = "a" and c = "-hcmod b" in hcmod_triangle_ineq [THEN add_right_mono])
-apply (simp add: hypreal_add_ac)
+apply (simp add: add_ac)
 done
 declare hcmod_triangle_ineq2 [simp]