--- a/src/HOL/Library/FSet.thy Sun Oct 16 22:43:51 2016 +0200
+++ b/src/HOL/Library/FSet.thy Mon Oct 17 11:46:22 2016 +0200
@@ -1011,7 +1011,7 @@
subsection \<open>Size setup\<close>
context includes fset.lifting begin
-lift_definition size_fset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a fset \<Rightarrow> nat" is "\<lambda>f. setsum (Suc \<circ> f)" .
+lift_definition size_fset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a fset \<Rightarrow> nat" is "\<lambda>f. sum (Suc \<circ> f)" .
end
instantiation fset :: (type) size begin
@@ -1030,7 +1030,7 @@
lemma fset_size_o_map: "inj f \<Longrightarrow> size_fset g \<circ> fimage f = size_fset (g \<circ> f)"
apply (subst fun_eq_iff)
- including fset.lifting by transfer (auto intro: setsum.reindex_cong subset_inj_on)
+ including fset.lifting by transfer (auto intro: sum.reindex_cong subset_inj_on)
setup \<open>
BNF_LFP_Size.register_size_global @{type_name fset} @{const_name size_fset}