src/HOL/Hyperreal/Poly.thy

--- a/src/HOL/Hyperreal/Poly.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/Poly.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -1023,7 +1023,7 @@
 apply (induct "p", auto)
 apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans)
 apply (rule abs_triangle_ineq)
-apply (auto intro!: mult_mono simp add: abs_mult, arith)
+apply (auto intro!: mult_mono simp add: abs_mult)
 done
 
 end