diff -r bf253f7075b4 -r 030f46b8c4b5 src/HOL/Hyperreal/HyperPow.thy
--- a/src/HOL/Hyperreal/HyperPow.thy	Thu Dec 14 21:03:39 2006 +0100
+++ b/src/HOL/Hyperreal/HyperPow.thy	Thu Dec 14 21:33:47 2006 +0100
@@ -202,7 +202,7 @@
 
 lemma hyperpow_realpow:
       "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
-by (simp add: star_of_def hypnat_of_nat_eq hyperpow)
+by transfer (rule refl)
 
 lemma hyperpow_SReal [simp]:
      "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"