diff -r db0f4f4c17c7 -r d7ff0a1df90a src/HOL/Library/Tree_Multiset.thy
--- a/src/HOL/Library/Tree_Multiset.thy	Tue Jun 16 20:50:00 2015 +0100
+++ b/src/HOL/Library/Tree_Multiset.thy	Wed Jun 17 17:21:11 2015 +0200
@@ -14,7 +14,7 @@
 "mset_tree Leaf = {#}" |
 "mset_tree (Node l a r) = {#a#} + mset_tree l + mset_tree r"
 
-lemma set_of_mset_tree[simp]: "set_of (mset_tree t) = set_tree t"
+lemma set_mset_tree[simp]: "set_mset (mset_tree t) = set_tree t"
 by(induction t) auto
 
 lemma size_mset_tree[simp]: "size(mset_tree t) = size t"