src/HOL/Library/Multiset.thy
changeset 55945 e96383acecf9
parent 55913 c1409c103b77
child 56656 7f9b686bf30a
--- a/src/HOL/Library/Multiset.thy	Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Mar 06 15:40:33 2014 +0100
@@ -2289,7 +2289,7 @@
 interpretation lifting_syntax .
 
 lemma set_of_transfer[transfer_rule]: "(pcr_multiset op = ===> op =) (\<lambda>f. {a. 0 < f a}) set_of"
-  unfolding set_of_def pcr_multiset_def cr_multiset_def fun_rel_def by auto
+  unfolding set_of_def pcr_multiset_def cr_multiset_def rel_fun_def by auto
 
 end