--- a/src/HOL/Library/Multiset.thy Mon Apr 03 19:41:17 2017 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Apr 03 22:18:56 2017 +0200
@@ -1894,7 +1894,7 @@
ultimately show ?case by simp
qed
-lemma mset_shuffle [simp]: "zs \<in> shuffle xs ys \<Longrightarrow> mset zs = mset xs + mset ys"
+lemma mset_shuffle: "zs \<in> shuffle xs ys \<Longrightarrow> mset zs = mset xs + mset ys"
by (induction xs ys arbitrary: zs rule: shuffle.induct) auto
lemma mset_insort [simp]: "mset (insort x xs) = add_mset x (mset xs)"