src/HOL/Inequalities.thy

--- a/src/HOL/Inequalities.thy	Mon Nov 30 14:24:51 2015 +0100
+++ b/src/HOL/Inequalities.thy	Tue Dec 01 14:09:10 2015 +0000
@@ -66,7 +66,6 @@
       using assms by (cases "i \<le> j") (auto simp: algebra_simps)
   } hence "?S \<le> 0"
     by (auto intro!: setsum_nonpos simp: mult_le_0_iff)
-       (auto simp: field_simps)
   finally show ?thesis by (simp add: algebra_simps)
 qed