--- a/src/HOL/Hyperreal/StarClasses.thy Wed Jun 06 19:12:59 2007 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy Wed Jun 06 20:49:04 2007 +0200
@@ -460,8 +460,10 @@
lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
by transfer (rule refl)
-instance star :: (ring_char_0) ring_char_0
-by (intro_classes, simp only: star_of_int_def star_of_eq of_int_eq_iff)
+instance star :: (semiring_char_0) semiring_char_0
+by (intro_classes, simp only: star_of_nat_def star_of_eq of_nat_eq_iff)
+
+instance star :: (ring_char_0) ring_char_0 ..
instance star :: (number_ring) number_ring
by (intro_classes, simp only: star_number_def star_of_int_def number_of_eq)