src/HOL/Rat.thy

--- a/src/HOL/Rat.thy	Tue Mar 10 11:56:32 2015 +0100
+++ b/src/HOL/Rat.thy	Tue Mar 10 15:20:40 2015 +0000
@@ -638,10 +638,6 @@
 
 subsection {* Embedding from Rationals to other Fields *}
 
-class field_char_0 = field + ring_char_0
-
-subclass (in linordered_field) field_char_0 ..
-
 context field_char_0
 begin