src/HOL/Finite_Set.thy

 apply simp
 done
 
 lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
 shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
-by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
+by (blast intro: finite_surj_inj subset_UNIV)
 
 lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
 shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
 by(fastsimp simp:surj_def dest!: endo_inj_surj)