diff -r 1e5585fd3632 -r 23e090051cb8 src/HOLCF/Cont.ML
--- a/src/HOLCF/Cont.ML	Mon Sep 06 22:12:08 1999 +0200
+++ b/src/HOLCF/Cont.ML	Tue Sep 07 10:40:58 1999 +0200
@@ -675,7 +675,7 @@
 by ( atac 1);
 by (rtac contlubI 1);
 by (strip_tac 1);
-by (forward_tac [chfin2finch] 1);
+by (ftac chfin2finch 1);
 by (rtac antisym_less 1);
 by ( force_tac (HOL_cs addIs [is_ub_thelub,ch2ch_monofun],
                HOL_ss addsimps [finite_chain_def,maxinch_is_thelub]) 1);