diff -r c6bae4456741 -r 489c1fbbb028 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Wed May 12 22:33:10 2010 -0700
+++ b/src/HOL/Algebra/Divisibility.thy	Thu May 13 14:34:05 2010 +0200
@@ -2193,7 +2193,7 @@
 
   from csmset msubset
       have "fmset G bs = fmset G as + fmset G cs"
-      by (simp add: multiset_eq_conv_count_eq mset_le_def)
+      by (simp add: multiset_ext_iff mset_le_def)
   hence basc: "b \<sim> a \<otimes> c"
       by (rule fmset_wfactors_mult) fact+