src/HOL/Library/Countable.thy
changeset 31992 f8aed98faae7
parent 30663 0b6aff7451b2
child 33640 0d82107dc07a
--- a/src/HOL/Library/Countable.thy	Fri Jul 10 09:24:50 2009 +0200
+++ b/src/HOL/Library/Countable.thy	Sun Jul 12 10:14:51 2009 +0200
@@ -58,7 +58,7 @@
 subclass (in finite) countable
 proof
   have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV)
-  with finite_conv_nat_seg_image [of UNIV]
+  with finite_conv_nat_seg_image [of "UNIV::'a set"]
   obtain n and f :: "nat \<Rightarrow> 'a" 
     where "UNIV = f ` {i. i < n}" by auto
   then have "surj f" unfolding surj_def by auto