src/HOL/Algebra/Divisibility.thy

       and csf: "wfactors G cs c"
       and csmset: "fmset G cs = fmset G bs - fmset G as" by auto
 
   from csmset msubset
       have "fmset G bs = fmset G as + fmset G cs"
-      by (simp add: multiset_ext_iff mset_le_def)
+      by (simp add: multiset_eq_iff mset_le_def)
   hence basc: "b \<sim> a \<otimes> c"
       by (rule fmset_wfactors_mult) fact+
 
   thus ?thesis
   proof (elim associatedE2)