diff -r 8eb6365f5916 -r b9a1486e79be src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Oct 16 22:43:51 2016 +0200
+++ b/src/HOL/List.thy	Mon Oct 17 11:46:22 2016 +0200
@@ -3808,12 +3808,12 @@
 lemma count_le_length: "count_list xs x \<le> length xs"
 by (induction xs) auto
 
-lemma setsum_count_set:
-  "set xs \<subseteq> X \<Longrightarrow> finite X \<Longrightarrow> setsum (count_list xs) X = length xs"
+lemma sum_count_set:
+  "set xs \<subseteq> X \<Longrightarrow> finite X \<Longrightarrow> sum (count_list xs) X = length xs"
 apply(induction xs arbitrary: X)
  apply simp
-apply (simp add: setsum.If_cases)
-by (metis Diff_eq setsum.remove)
+apply (simp add: sum.If_cases)
+by (metis Diff_eq sum.remove)
 
 
 subsubsection \<open>@{const List.extract}\<close>