src/HOL/Library/Multiset.thy

--- a/src/HOL/Library/Multiset.thy	Wed Feb 18 22:46:48 2015 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Feb 19 11:53:36 2015 +0100
@@ -1963,7 +1963,7 @@
   by (fact add_left_cancel)
 
 lemma multi_union_self_other_eq: "(A::'a multiset) + X = A + Y \<Longrightarrow> X = Y"
-  by (fact add_imp_eq)
+  by (fact add_left_imp_eq)
 
 lemma mset_less_trans: "(M::'a multiset) < K \<Longrightarrow> K < N \<Longrightarrow> M < N"
   by (fact order_less_trans)