--- a/src/HOL/Library/Univ_Poly.thy Fri Feb 05 14:33:31 2010 +0100
+++ b/src/HOL/Library/Univ_Poly.thy Fri Feb 05 14:33:50 2010 +0100
@@ -990,7 +990,7 @@
text{*bound for polynomial.*}
-lemma poly_mono: "abs(x) \<le> k ==> abs(poly p (x::'a::{ordered_idom})) \<le> poly (map abs p) k"
+lemma poly_mono: "abs(x) \<le> k ==> abs(poly p (x::'a::{linordered_idom})) \<le> poly (map abs p) k"
apply (induct "p", auto)
apply (rule_tac y = "abs a + abs (x * poly p x)" in order_trans)
apply (rule abs_triangle_ineq)