diff -r 4ccb7e635477 -r e68a0b651eb5 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Mon Sep 05 15:00:37 2016 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Mon Sep 05 15:47:50 2016 +0200
@@ -2051,11 +2051,11 @@
     from cP csP
         have tP: "\<forall>x\<in>set (c#cs). P x" by simp
     from mset a
-    have "mset (map (assocs G) (c#cs)) = mset Cs' + {#a#}" by simp
+    have "mset (map (assocs G) (c#cs)) = add_mset a (mset Cs')" by simp
     from tP this
     show "\<exists>cs. (\<forall>x\<in>set cs. P x) \<and>
                mset (map (assocs G) cs) =
-               mset Cs' + {#a#}" by fast
+               add_mset a (mset Cs')" by fast
   qed
   thus ?thesis by (simp add: fmset_def)
 qed