diff -r d7e6c7760db5 -r fd26519b1a6a src/HOL/Library/Tree_Multiset.thy
--- a/src/HOL/Library/Tree_Multiset.thy	Mon Jul 27 23:56:11 2015 +0200
+++ b/src/HOL/Library/Tree_Multiset.thy	Tue Jul 28 13:00:54 2015 +0200
@@ -35,9 +35,4 @@
 lemma map_mirror: "mset_tree (mirror t) = mset_tree t"
 by (induction t) (simp_all add: ac_simps)
 
-lemma del_rightmost_mset_tree:
-  "\<lbrakk> del_rightmost t = (t',x);  t \<noteq> \<langle>\<rangle> \<rbrakk> \<Longrightarrow> mset_tree t = {#x#} + mset_tree t'"
-apply(induction t arbitrary: t' rule: del_rightmost.induct)
-by (auto split: prod.splits) (auto simp: ac_simps)
-
 end