diff -r eebe69f31474 -r 58043346ca64 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Power.thy	Tue Mar 31 21:54:32 2015 +0200
@@ -705,7 +705,7 @@
 
 text{*Perhaps these should be simprules.*}
 lemma power_inverse:
-  fixes a :: "'a::division_ring_inverse_zero"
+  fixes a :: "'a::division_ring"
   shows "inverse (a ^ n) = inverse a ^ n"
 apply (cases "a = 0")
 apply (simp add: power_0_left)
@@ -713,11 +713,11 @@
 done (* TODO: reorient or rename to inverse_power *)
 
 lemma power_one_over:
-  "1 / (a::'a::{field_inverse_zero, power}) ^ n =  (1 / a) ^ n"
+  "1 / (a::'a::{field, power}) ^ n =  (1 / a) ^ n"
   by (simp add: divide_inverse) (rule power_inverse)
 
 lemma power_divide [field_simps, divide_simps]:
-  "(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n"
+  "(a / b) ^ n = (a::'a::field) ^ n / b ^ n"
 apply (cases "b = 0")
 apply (simp add: power_0_left)
 apply (rule nonzero_power_divide)