diff -r 8c240fdeffcb -r 5840724b1d71 src/HOL/Library/DAList_Multiset.thy
--- a/src/HOL/Library/DAList_Multiset.thy	Sun Sep 23 21:49:31 2018 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy	Mon Sep 24 14:30:09 2018 +0200
@@ -372,7 +372,7 @@
 
 end
 
-\<comment> \<open>we cannot use \<open>\<lambda>a n. (+) (a * n)\<close> for folding, since \<open>( * )\<close> is not defined in \<open>comm_monoid_add\<close>\<close>
+\<comment> \<open>we cannot use \<open>\<lambda>a n. (+) (a * n)\<close> for folding, since \<open>(*)\<close> is not defined in \<open>comm_monoid_add\<close>\<close>
 lemma sum_mset_Bag[code]: "sum_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (((+) a) ^^ n)) 0 ms"
   unfolding sum_mset.eq_fold
   apply (rule comp_fun_commute.DAList_Multiset_fold)
@@ -380,8 +380,8 @@
   apply (auto simp: ac_simps)
   done
 
-\<comment> \<open>we cannot use \<open>\<lambda>a n. ( * ) (a ^ n)\<close> for folding, since \<open>(^)\<close> is not defined in \<open>comm_monoid_mult\<close>\<close>
-lemma prod_mset_Bag[code]: "prod_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. ((( * ) a) ^^ n)) 1 ms"
+\<comment> \<open>we cannot use \<open>\<lambda>a n. (*) (a ^ n)\<close> for folding, since \<open>(^)\<close> is not defined in \<open>comm_monoid_mult\<close>\<close>
+lemma prod_mset_Bag[code]: "prod_mset (Bag ms) = DAList_Multiset.fold (\<lambda>a n. (((*) a) ^^ n)) 1 ms"
   unfolding prod_mset.eq_fold
   apply (rule comp_fun_commute.DAList_Multiset_fold)
   apply unfold_locales