--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Tue Mar 10 18:32:37 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Tue Mar 10 18:33:13 1998 +0100
@@ -920,12 +920,12 @@
by (res_inst_tac [("t","s2")] (seq.reach RS subst) 1);
by (rtac (fix_def2 RS ssubst ) 1);
by (stac contlub_cfun_fun 1);
-by (rtac is_chain_iterate 1);
+by (rtac chain_iterate 1);
by (stac contlub_cfun_fun 1);
-by (rtac is_chain_iterate 1);
+by (rtac chain_iterate 1);
by (rtac lub_mono 1);
-by (rtac (is_chain_iterate RS ch2ch_fappL) 1);
-by (rtac (is_chain_iterate RS ch2ch_fappL) 1);
+by (rtac (chain_iterate RS ch2ch_fappL) 1);
+by (rtac (chain_iterate RS ch2ch_fappL) 1);
by (rtac allI 1);
by (resolve_tac prems 1);
qed"take_lemma_less1";