src/HOLCF/Fix.thy

--- a/src/HOLCF/Fix.thy	Tue Jun 14 04:04:09 2005 +0200
+++ b/src/HOLCF/Fix.thy	Tue Jun 14 04:05:15 2005 +0200
@@ -100,7 +100,7 @@
 by (induct_tac n, simp_all)
 
 lemma cont_iterate: "cont (iterate n)"
-by (rule cont_iterate1 [THEN cont2cont_CF1L_rev2])
+by (rule cont_iterate1 [THEN cont2cont_lambda])
 
 lemmas monofun_iterate2 = cont_iterate2 [THEN cont2mono, standard]
 lemmas contlub_iterate2 = cont_iterate2 [THEN cont2contlub, standard]