src/HOL/Complex/CLim.thy

--- a/src/HOL/Complex/CLim.thy	Wed Sep 27 16:33:08 2006 +0200
+++ b/src/HOL/Complex/CLim.thy	Wed Sep 27 18:34:26 2006 +0200
@@ -985,6 +985,6 @@
 lemma CARAT_CDERIVD:
      "(\<forall>z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l
       ==> NSCDERIV f x :> l"
-by (auto simp add: NSCDERIV_iff2 isNSContc_def cstarfun_if_eq); 
+by (auto simp add: NSCDERIV_iff2 isNSContc_def starfun_if_eq); 
 
 end