diff -r 7f562aa4eb4b -r 86e7560e07d0 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Thu Aug 06 23:56:48 2015 +0200
@@ -441,12 +441,12 @@
 
 lemma hyperpow_not_zero:
   "\<And>r n. r \<noteq> (0::'a::{field} star) ==> r pow n \<noteq> 0"
-by transfer (rule field_power_not_zero)
+by transfer (rule power_not_zero)
 
 lemma hyperpow_inverse:
   "\<And>r n. r \<noteq> (0::'a::field star)
    \<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
-by transfer (rule power_inverse)
+by transfer (rule power_inverse [symmetric])
 
 lemma hyperpow_hrabs:
   "\<And>r n. abs (r::'a::{linordered_idom} star) pow n = abs (r pow n)"