diff -r bc7982c54e37 -r d323e7773aa8 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Mon Apr 26 11:34:19 2010 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Mon Apr 26 15:37:50 2010 +0200
@@ -140,12 +140,12 @@
 
 lemma of_hypreal_inverse [simp]:
   "\<And>x. of_hypreal (inverse x) =
-   inverse (of_hypreal x :: 'a::{real_div_algebra,division_ring_inverse_zero} star)"
+   inverse (of_hypreal x :: 'a::{real_div_algebra, division_ring_inverse_zero} star)"
 by transfer (rule of_real_inverse)
 
 lemma of_hypreal_divide [simp]:
   "\<And>x y. of_hypreal (x / y) =
-   (of_hypreal x / of_hypreal y :: 'a::{real_field,division_ring_inverse_zero} star)"
+   (of_hypreal x / of_hypreal y :: 'a::{real_field, field_inverse_zero} star)"
 by transfer (rule of_real_divide)
 
 lemma of_hypreal_eq_iff [simp]:
@@ -454,7 +454,7 @@
 by transfer (rule field_power_not_zero)
 
 lemma hyperpow_inverse:
-  "\<And>r n. r \<noteq> (0::'a::{division_ring_inverse_zero,field} star)
+  "\<And>r n. r \<noteq> (0::'a::field_inverse_zero star)
    \<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
 by transfer (rule power_inverse)