diff -r ed7d12bcf8f8 -r 108662d50512 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Fri Feb 05 14:33:31 2010 +0100
+++ b/src/HOL/Archimedean_Field.thy	Fri Feb 05 14:33:50 2010 +0100
@@ -12,7 +12,7 @@
 
 text {* Archimedean fields have no infinite elements. *}
 
-class archimedean_field = ordered_field + number_ring +
+class archimedean_field = linordered_field + number_ring +
   assumes ex_le_of_int: "\<exists>z. x \<le> of_int z"
 
 lemma ex_less_of_int: