diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -2269,13 +2269,13 @@
   "prod_mset (replicate_mset n a) = a ^ n"
   by (induct n) simp_all
 
-lemma setprod_unfold_prod_mset:
-  "setprod f A = prod_mset (image_mset f (mset_set A))"
+lemma prod_unfold_prod_mset:
+  "prod f A = prod_mset (image_mset f (mset_set A))"
   by (cases "finite A") (induct A rule: finite_induct, simp_all)
 
 lemma prod_mset_multiplicity:
-  "prod_mset M = setprod (\<lambda>x. x ^ count M x) (set_mset M)"
-  by (simp add: fold_mset_def setprod.eq_fold prod_mset.eq_fold funpow_times_power comp_def)
+  "prod_mset M = prod (\<lambda>x. x ^ count M x) (set_mset M)"
+  by (simp add: fold_mset_def prod.eq_fold prod_mset.eq_fold funpow_times_power comp_def)
 
 lemma prod_mset_delta: "prod_mset (image_mset (\<lambda>x. if x = y then c else 1) A) = c ^ count A y"
   by (induction A) simp_all