diff -r 670063003ad3 -r 85f38d5f8807 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Feb 09 09:21:10 2016 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Feb 10 18:43:19 2016 +0100
@@ -302,7 +302,7 @@
    apply (auto intro: multiset_eq_iff [THEN iffD2])
   done
 
-interpretation subset_mset: ordered_cancel_comm_monoid_diff  "op +" "op -" 0 "op \<le>#" "op <#"
+interpretation subset_mset: ordered_cancel_comm_monoid_diff  "op +" 0 "op \<le>#" "op <#" "op -"
   by standard (simp, fact mset_le_exists_conv)
 
 lemma mset_le_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<le># B + C \<longleftrightarrow> A \<le># B"