diff -r e2be3370ae03 -r e0fb46018187 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Jun 14 00:22:10 2025 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat Jun 14 11:45:56 2025 +0200
@@ -4332,8 +4332,8 @@
 lemma [code]: "filter_mset f (mset xs) = mset (filter f xs)"
   by simp
 
-lemma [code]: "mset xs - mset ys = mset (fold remove1 ys xs)"
-  by (rule sym, induct ys arbitrary: xs) (simp_all add: diff_add diff_right_commute diff_diff_add)
+lemma [code]: "mset xs - mset ys = mset (minus_list_mset xs ys)"
+  by simp
 
 lemma [code]:
   "mset xs \<inter># mset ys =