1.1 --- a/src/HOL/Library/Multiset.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -108,7 +108,7 @@
     1.4  
     1.5  theorems union_ac = union_assoc union_commute union_lcomm
     1.6  
     1.7 -instance multiset :: (type) plus_ac0
     1.8 +instance multiset :: (type) comm_monoid_add
     1.9  proof 
    1.10    fix a b c :: "'a multiset"
    1.11    show "(a + b) + c = a + (b + c)" by (rule union_assoc)