diff -r c2524d123528 -r 7e6ffd8f51a9 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Mon Apr 27 08:22:37 2009 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Mon Apr 27 10:11:44 2009 +0200
@@ -426,7 +426,7 @@
 
 subsection{*Powers with Hypernatural Exponents*}
 
-definition pow :: "['a::recpower star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
+definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
   hyperpow_def [transfer_unfold, code del]: "R pow N = ( *f2* op ^) R N"
   (* hypernatural powers of hyperreals *)
 
@@ -459,7 +459,7 @@
 by transfer (rule power_add)
 
 lemma hyperpow_one [simp]:
-  "\<And>r. (r::'a::recpower star) pow (1::hypnat) = r"
+  "\<And>r. (r::'a::monoid_mult star) pow (1::hypnat) = r"
 by transfer (rule power_one_right)
 
 lemma hyperpow_two: