diff -r 86f598f84188 -r e40e9e9769f4 src/HOLCF/Fun_Cpo.thy
--- a/src/HOLCF/Fun_Cpo.thy	Wed Nov 17 12:19:19 2010 -0800
+++ b/src/HOLCF/Fun_Cpo.thy	Wed Nov 17 16:05:18 2010 -0800
@@ -46,11 +46,6 @@
 
 subsection {* Full function space is chain complete *}
 
-text {* Function application is monotone. *}
-
-lemma monofun_app: "monofun (\<lambda>f. f x)"
-by (rule monofunI, simp add: below_fun_def)
-
 text {* Properties of chains of functions. *}
 
 lemma fun_chain_iff: "chain S \<longleftrightarrow> (\<forall>x. chain (\<lambda>i. S i x))"
@@ -158,6 +153,9 @@
 apply (simp add: cont2contlubE thelub_fun ch2ch_cont)
 done
 
+lemma cont_fun: "cont (\<lambda>f. f x)"
+using cont_id by (rule cont2cont_fun)
+
 text {*
   Lambda abstraction preserves monotonicity and continuity.
   (Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"}.)