--- a/src/HOL/Complex/CStar.thy	Thu Dec 14 18:10:38 2006 +0100
+++ b/src/HOL/Complex/CStar.thy	Thu Dec 14 19:15:16 2006 +0100
@@ -22,7 +22,7 @@
 
 subsection{*Theorems about Nonstandard Extensions of Functions*}
 
-lemma starfunC_hcpow: "!!Z. ( *f* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n"
+lemma starfunC_hcpow: "!!Z. ( *f* (%z. z ^ n)) Z = Z pow hypnat_of_nat n"
 by transfer (rule refl)
 
 lemma starfunCR_cmod: "*f* cmod = hcmod"