diff -r d73f67e90a95 -r 27509e72f29e src/HOL/Complex/CLim.thy
--- a/src/HOL/Complex/CLim.thy	Tue Sep 13 23:30:01 2005 +0200
+++ b/src/HOL/Complex/CLim.thy	Wed Sep 14 01:47:06 2005 +0200
@@ -351,10 +351,10 @@
 (*** NSCLIM_not zero and hence CLIM_not_zero ***)
 
 lemma NSCLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --NSC> 0)"
-apply (auto simp del: hcomplex_of_complex_zero simp add: NSCLIM_def)
+apply (auto simp del: star_of_zero simp add: NSCLIM_def)
 apply (rule_tac x = "hcomplex_of_complex x + hcomplex_of_hypreal epsilon" in exI)
 apply (auto intro: CInfinitesimal_add_capprox_self [THEN capprox_sym]
-            simp del: hcomplex_of_complex_zero)
+            simp del: star_of_zero)
 done
 
 (* [| k \<noteq> 0; (%x. k) -- x --NSC> 0 |] ==> R *)