diff -r e78d1e06d855 -r 71c8973a604b src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Mon May 17 18:51:25 2010 -0700
+++ b/src/HOL/Big_Operators.thy	Mon May 17 18:59:59 2010 -0700
@@ -673,7 +673,7 @@
   proof induct
     case empty thus ?case by simp
   next
-    case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg)
+    case (insert x A) thus ?case by auto
   qed
 next
   case False thus ?thesis by (simp add: setsum_def)