diff -r 29cf40fe8daf -r a89b4bc311a5 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/NSA/HyperDef.thy	Sun Nov 20 21:05:23 2011 +0100
@@ -422,7 +422,7 @@
 lemma power_hypreal_of_real_number_of:
      "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)"
 by simp
-declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp]
+declare power_hypreal_of_real_number_of [of _ "number_of w", simp] for w
 (*
 lemma hrealpow_HFinite:
   fixes x :: "'a::{real_normed_algebra,power} star"