use algebra_simps instead of ring_simps

--- a/src/HOL/Integration.thy	Tue Jun 02 14:00:24 2009 +0200
+++ b/src/HOL/Integration.thy	Tue Jun 02 14:37:05 2009 +0200
@@ -432,7 +432,7 @@
     have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f"
       using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto
     also have "\<dots> = rsum D1 f + rsum D2 f"
-      by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append ring_simps)
+      by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps)
     finally have "\<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>"
       using add_strict_mono[OF rsum1 rsum2] by simp
   }