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 "\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 \ 'b"