diff -r 87fbfea0bd0a -r 6e83d94760c4 src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Sat Jun 27 20:26:33 2015 +0200
+++ b/src/HOL/Library/Permutations.thy	Sun Jun 28 14:30:53 2015 +0200
@@ -44,8 +44,11 @@
 lemma permutes_surj: "p permutes s \<Longrightarrow> surj p"
   unfolding permutes_def surj_def by metis
 
+lemma permutes_bij: "p permutes s \<Longrightarrow> bij p"
+unfolding bij_def by (metis permutes_inj permutes_surj)
+
 lemma permutes_imp_bij: "p permutes S \<Longrightarrow> bij_betw p S S"
-  by (metis UNIV_I bij_betw_def permutes_image permutes_inj subsetI subset_inj_on)
+by (metis UNIV_I bij_betw_subset permutes_bij permutes_image subsetI)
 
 lemma bij_imp_permutes: "bij_betw p S S \<Longrightarrow> (\<And>x. x \<notin> S \<Longrightarrow> p x = x) \<Longrightarrow> p permutes S"
   unfolding permutes_def bij_betw_def inj_on_def