instance fun :: (finite, countable) countable

--- a/src/HOL/Library/Countable.thy	Sun Mar 09 07:57:30 2008 +0100
+++ b/src/HOL/Library/Countable.thy	Mon Mar 10 18:44:20 2008 +0100
@@ -180,4 +180,18 @@
   qed
 qed
 
+
+text {* Functions *}
+
+instance "fun" :: (finite, countable) countable
+proof
+  obtain xs :: "'a list" where xs: "set xs = UNIV"
+    using finite_list [OF finite_UNIV] ..
+  show "\<exists>to_nat::('a \<Rightarrow> 'b) \<Rightarrow> nat. inj to_nat"
+  proof
+    show "inj (\<lambda>f. to_nat (map f xs))"
+      by (rule injI, simp add: xs expand_fun_eq)
+  qed
+qed
+
 end