| changeset 60495 | d7ff0a1df90a | 
| parent 60397 | f8a513fedb31 | 
| child 60502 | aa58872267ee | 
--- a/src/HOL/Library/Permutation.thy Tue Jun 16 20:50:00 2015 +0100 +++ b/src/HOL/Library/Permutation.thy Wed Jun 17 17:21:11 2015 +0200 @@ -136,7 +136,7 @@ apply (erule perm.trans) apply (rule perm_sym) apply (erule perm_remove) - apply (drule_tac f=set_of in arg_cong) + apply (drule_tac f=set_mset in arg_cong) apply simp done