src/HOL/Library/Extended_Nat.thy

--- a/src/HOL/Library/Extended_Nat.thy	Sun Oct 16 22:43:51 2016 +0200
+++ b/src/HOL/Library/Extended_Nat.thy	Mon Oct 17 11:46:22 2016 +0200
@@ -17,7 +17,7 @@
 begin
 
 lemma sums_SUP[simp, intro]: "f sums (SUP n. \<Sum>i<n. f i)"
-  unfolding sums_def by (intro LIMSEQ_SUP monoI setsum_mono2 zero_le) auto
+  unfolding sums_def by (intro LIMSEQ_SUP monoI sum_mono2 zero_le) auto
 
 lemma suminf_eq_SUP: "suminf f = (SUP n. \<Sum>i<n. f i)"
   using sums_SUP by (rule sums_unique[symmetric])