src/HOL/Library/Fraction_Field.thy

--- a/src/HOL/Library/Fraction_Field.thy	Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Library/Fraction_Field.thy	Tue Mar 31 21:54:32 2015 +0200
@@ -224,7 +224,7 @@
 
 end
 
-instantiation fract :: (idom) field_inverse_zero
+instantiation fract :: (idom) field
 begin
 
 definition inverse_fract_def:
@@ -428,7 +428,7 @@
 
 end
 
-instance fract :: (linordered_idom) linordered_field_inverse_zero
+instance fract :: (linordered_idom) linordered_field
 proof
   fix q r s :: "'a fract"
   assume "q \<le> r"