--- a/src/HOL/Library/Multiset.thy Mon Mar 22 10:49:51 2021 +0000 +++ b/src/HOL/Library/Multiset.thy Mon Mar 22 12:18:43 2021 +0000 @@ -2333,7 +2333,7 @@ end -context ordered_cancel_comm_monoid_diff +context cancel_comm_monoid_add begin lemma sum_mset_diff: