diff -r 21d71d20f64e -r cf7669049df5 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Thu Nov 03 01:54:51 2005 +0100
+++ b/src/HOLCF/domain/theorems.ML	Thu Nov 03 02:19:48 2005 +0100
@@ -107,7 +107,7 @@
   fun appl_of_def def = let
         val (_ $ con $ lam) = concl_of def;
         val (vars, rhs) = arglist lam;
-        val lhs = mk_cRep_CFun (con, bound_vars (length vars));
+        val lhs = list_ccomb (con, bound_vars (length vars));
         val appl = bind_fun vars (lhs == rhs);
         val cs = ContProc.cont_thms lam;
         val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs;
@@ -158,7 +158,7 @@
 local 
   fun bind_fun t = Library.foldr mk_All (when_funs cons,t);
   fun bound_fun i _ = Bound (length cons - i);
-  val when_app  = Library.foldl (op `) (%%:(dname^"_when"), mapn bound_fun 1 cons);
+  val when_app  = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons);
 in
 val when_strict = pg [when_appl, mk_meta_eq rep_strict]
 			(bind_fun(mk_trp(strict when_app)))
@@ -166,7 +166,7 @@
 val when_apps = let fun one_when n (con,args) = pg (when_appl :: con_appls)
                 (bind_fun (lift_defined %: (nonlazy args, 
                 mk_trp(when_app`(con_app con args) ===
-                       mk_cRep_CFun(bound_fun n 0,map %# args)))))[
+                       list_ccomb(bound_fun n 0,map %# args)))))[
                 asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1];
         in mapn one_when 1 cons end;
 end;
@@ -224,7 +224,7 @@
   let
     val rules = [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE];
     fun one_compact (con,args) = pg con_appls
-      (lift (fn x => %%:compactN $ %:(vname x)) (args, mk_trp(%%:compactN $ (con_app con args))))
+      (lift (fn x => %%:compactN $ %#x) (args, mk_trp(%%:compactN $ (con_app con args))))
       [rtac (iso_locale RS iso_compact_abs) 1, REPEAT (resolve_tac rules 1 ORELSE atac 1)];
   in map one_compact cons end;
 
@@ -391,11 +391,11 @@
 local
   val iterate_Cprod_ss = simpset_of Fix.thy;
   val copy_con_rews  = copy_rews @ con_rews;
-  val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
+  val copy_take_defs = (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
   val take_stricts=pg copy_take_defs(mk_trp(foldr1 mk_conj(map(fn((dn,args),_)=>
             strict(dc_take dn $ %:"n")) eqs))) ([
                         induct_tac "n" 1,
-                         simp_tac iterate_Cprod_ss 1,
+                        simp_tac iterate_Cprod_ss 1,
                         asm_simp_tac (iterate_Cprod_ss addsimps copy_rews)1]);
   val take_stricts' = rewrite_rule copy_take_defs take_stricts;
   val take_0s = mapn(fn n=> fn dn => pg axs_take_def(mk_trp((dc_take dn $ %%:"0")