diff -r e26ec695c9b3 -r dfc459989d24 src/HOL/Hyperreal/StarClasses.thy
--- 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)