--- a/src/HOL/Library/Multiset.thy Mon Mar 22 00:07:55 2021 +0100 +++ b/src/HOL/Library/Multiset.thy Mon Mar 22 12:18:35 2021 +0000 @@ -2329,7 +2329,7 @@ end -context ordered_cancel_comm_monoid_diff +context cancel_comm_monoid_add begin lemma sum_mset_diff: