
diff -r 49b9d301fadb -r 8adc57fb8454 src/HOLCF/Fun_Cpo.thy
--- a/src/HOLCF/Fun_Cpo.thy	Fri Oct 22 06:08:51 2010 -0700
+++ b/src/HOLCF/Fun_Cpo.thy	Fri Oct 22 06:58:45 2010 -0700
@@ -128,8 +128,6 @@
   thus "\<exists>n. max_in_chain n Y" ..
 qed
 
-instance "fun" :: (finite, finite_po) finite_po ..
-
 instance "fun" :: (type, discrete_cpo) discrete_cpo
 proof
   fix f g :: "'a \<Rightarrow> 'b"




