diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/domain/theorems.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -41,7 +41,7 @@
                                 asm_simp_tac (HOLCF_ss addsimps rews) i;
 
 val chain_tac = REPEAT_DETERM o resolve_tac 
-                [chain_iterate, ch2ch_fappR, ch2ch_fappL];
+                [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL];
 
 (* ----- general proofs ----------------------------------------------------- *)
 
@@ -175,7 +175,7 @@
 val when_apps = let fun one_when n (con,args) = pg axs_con_def 
                 (bind_fun (lift_defined % (nonlazy args, 
                 mk_trp(when_app`(con_app con args) ===
-                       mk_cfapp(bound_fun n 0,map %# args)))))[
+                       mk_cRep_CFun(bound_fun n 0,map %# args)))))[
                 asm_simp_tac (HOLCF_ss addsimps [when_appl,ax_abs_iso]) 1];
         in mapn one_when 1 cons end;
 end;