src/HOLCF/Cfun.thy
changeset 40089 8adc57fb8454
parent 40046 ba2e41c8b725
child 40091 1ca61fbd8a79
--- a/src/HOLCF/Cfun.thy	Fri Oct 22 06:08:51 2010 -0700
+++ b/src/HOLCF/Cfun.thy	Fri Oct 22 06:58:45 2010 -0700
@@ -95,10 +95,7 @@
 lemma UU_CFun: "\<bottom> \<in> CFun"
 by (simp add: CFun_def inst_fun_pcpo)
 
-instance cfun :: (finite_po, finite_po) finite_po
-by (rule typedef_finite_po [OF type_definition_CFun])
-
-instance cfun :: (finite_po, chfin) chfin
+instance cfun :: ("{finite,cpo}", chfin) chfin
 by (rule typedef_chfin [OF type_definition_CFun below_CFun_def])
 
 instance cfun :: (cpo, discrete_cpo) discrete_cpo