diff -r 16733b31e1cf -r 49c312eaaa11 src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Aug 02 13:48:21 2006 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Aug 02 16:50:41 2006 +0200
@@ -187,6 +187,8 @@
     by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP)
 qed
 
+ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
+
 lemma coeff_mult [simp]:
   "coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)"
 proof -
@@ -226,6 +228,8 @@
     by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP)
 qed
 
+ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
+
 lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)"
 by (unfold up_uminus_def) (simp add: ring_simps)