# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1491250736 -7200
# Node ID 4ff2ba82d6681143c26924f604eecd0f88a43b0a
# Parent  ac9391e04ef2f59b64e5b5f821b93641fe615b31
removed problematic simp rule

diff -r ac9391e04ef2 -r 4ff2ba82d668 src/HOL/Library/Multiset.thy
--- 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)"