diff -r f9aa43287e42 -r c2adeb1bae5c src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Thu Jan 03 23:59:51 2008 +0100
+++ b/src/HOLCF/Cfun.thy	Fri Jan 04 00:01:02 2008 +0100
@@ -103,6 +103,12 @@
 lemma UU_CFun: "\<bottom> \<in> CFun"
 by (simp add: CFun_def inst_fun_pcpo cont_const)
 
+instance "->" :: (finite_po, finite_po) finite_po
+by (rule typedef_finite_po [OF type_definition_CFun])
+
+instance "->" :: (finite_po, chfin) chfin
+by (rule typedef_chfin [OF type_definition_CFun less_CFun_def])
+
 instance "->" :: (cpo, pcpo) pcpo
 by (rule typedef_pcpo [OF type_definition_CFun less_CFun_def UU_CFun])