--- a/src/HOL/Finite_Set.thy Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Finite_Set.thy Mon Nov 22 10:34:33 2010 +0100
@@ -2286,7 +2286,7 @@
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"