1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Tue Feb 09 16:07:09 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Feb 10 08:49:25 2010 +0100
     1.3 @@ -2950,7 +2950,8 @@
     1.4                 (\<Sum> i = 0..<Suc n. inverse (real (\<Prod> j \<in> {k..<k+i}. j)) * ?f i (real c) * (xs!x - real c)^i) +
     1.5                 inverse (real (\<Prod> j \<in> {k..<k+Suc n}. j)) * ?f (Suc n) t * (xs!x - real c)^Suc n" (is "_ = ?T")
     1.6          unfolding funpow_Suc C_def[symmetric] setsum_move0 setprod_head_Suc
     1.7 -        by (auto simp add: algebra_simps setsum_right_distrib[symmetric])
     1.8 +        by (auto simp add: algebra_simps)
     1.9 +          (simp only: mult_left_commute [of _ "inverse (real k)"] setsum_right_distrib [symmetric])
    1.10        finally have "?T \<in> {real l .. real u}" . }
    1.11      thus ?thesis using DERIV by blast
    1.12    qed