diff -r 942438a0fa84 -r a19ba9bbc8dc src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Tue Apr 27 08:18:25 2010 +0200
+++ b/src/HOL/NSA/StarDef.thy	Tue Apr 27 09:49:36 2010 +0200
@@ -950,10 +950,7 @@
 
 instance star :: (linordered_idom) linordered_idom ..
 instance star :: (linordered_field) linordered_field ..
-instance star :: (linordered_field_inverse_zero) linordered_field_inverse_zero 
-apply intro_classes
-apply (rule inverse_zero)
-done
+instance star :: (linordered_field_inverse_zero) linordered_field_inverse_zero ..
 
 
 subsection {* Power *}