src/HOL/Quotient_Examples/Quotient_Rat.thy

--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Sat Mar 24 16:27:04 2012 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Sun Mar 25 20:15:39 2012 +0200
@@ -159,17 +159,6 @@
   apply auto
   done
 
-instantiation rat :: number_ring
-begin
-
-definition
-  rat_number_of_def: "number_of w = Fract w 1"
-
-instance apply default
-  unfolding rat_number_of_def of_int_rat ..
-
-end
-
 instantiation rat :: field_inverse_zero begin
 
 fun rat_inverse_raw where