diff -r 0a01efff43e9 -r 7ad150f5fc10 src/HOLCF/Cfun2.ML
--- a/src/HOLCF/Cfun2.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/HOLCF/Cfun2.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -94,9 +94,9 @@
 (* ?x2 << ?x1 ==> ?fo5$?x2 << ?fo5$?x1                                      *)
 
 Goal "chain Y ==> chain (%i. f\\<cdot>(Y i))";
-br chainI 1;
-br monofun_cfun_arg 1;
-be chainE 1;
+by (rtac chainI 1);
+by (rtac monofun_cfun_arg 1);
+by (etac chainE 1);
 qed "chain_monofun";