src/HOL/Power.thy

--- a/src/HOL/Power.thy	Fri Jan 14 15:43:04 2011 +0100
+++ b/src/HOL/Power.thy	Fri Jan 14 15:44:47 2011 +0100
@@ -297,7 +297,7 @@
   assume "~ a \<le> b"
   then have "b < a" by (simp only: linorder_not_le)
   then have "b ^ Suc n < a ^ Suc n"
-    by (simp only: prems power_strict_mono)
+    by (simp only: assms power_strict_mono)
   from le and this show False
     by (simp add: linorder_not_less [symmetric])
 qed