diff -r d4f1d6ef119c -r 84f0996a530b src/HOL/Hyperreal/StarClasses.thy
--- a/src/HOL/Hyperreal/StarClasses.thy	Tue Jul 03 18:42:09 2007 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy	Tue Jul 03 20:26:08 2007 +0200
@@ -365,7 +365,7 @@
 instance star :: (ring_1) ring_1 ..
 instance star :: (comm_ring_1) comm_ring_1 ..
 instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
-instance star :: (dom) dom ..
+instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
 instance star :: (idom) idom .. 
 
 instance star :: (division_ring) division_ring