diff -r 695a2365d32f -r 4a8c3f8b0a92 src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Tue Oct 11 17:30:00 2005 +0200
+++ b/src/HOLCF/Cont.thy	Tue Oct 11 23:19:50 2005 +0200
@@ -215,7 +215,7 @@
 
 lemma mono2mono_MF1L_rev: "\<forall>y. monofun (\<lambda>x. f x y) \<Longrightarrow> monofun f"
 apply (rule monofunI)
-apply (rule less_fun [THEN iffD2])
+apply (rule less_fun_ext)
 apply (blast dest: monofunE)
 done