src/ZF/ex/Limit.thy

--- a/src/ZF/ex/Limit.thy	Wed Jul 10 16:07:52 2002 +0200
+++ b/src/ZF/ex/Limit.thy	Wed Jul 10 16:54:07 2002 +0200
@@ -748,8 +748,7 @@
 
 lemma cf_least:
     "[|cpo(D); pcpo(E); y \<in> cont(D,E)|]==>rel(cf(D,E),(\<lambda>x \<in> set(D).bot(E)),y)"
-apply (rule rel_cfI, simp)
-apply typecheck
+apply (rule rel_cfI, simp, typecheck)
 done
 
 lemma pcpo_cf: