src/HOL/Fields.thy

--- a/src/HOL/Fields.thy	Mon Aug 26 23:39:53 2013 +0200
+++ b/src/HOL/Fields.thy	Tue Aug 27 14:37:56 2013 +0200
@@ -842,7 +842,7 @@
 lemma gt_half_sum: "a < b ==> (a+b)/(1+1) < b"
 by (simp add: field_simps zero_less_two)
 
-subclass dense_linorder
+subclass unbounded_dense_linorder
 proof
   fix x y :: 'a
   from less_add_one show "\<exists>y. x < y" ..