# HG changeset patch
# User oheimb
# Date 890751282 -3600
# Node ID 2c090aef2ca2c9314d13b52977dfbe50ae12163a
# Parent  b3aab5c73b5260467e111a3b3468de65e6f32544
added cproj', and therefore extended prj

diff -r b3aab5c73b52 -r 2c090aef2ca2 src/HOLCF/domain/library.ML
--- a/src/HOLCF/domain/library.ML	Tue Mar 24 15:53:47 1998 +0100
+++ b/src/HOLCF/domain/library.ML	Tue Mar 24 15:54:42 1998 +0100
@@ -153,11 +153,17 @@
 fun con_app con = con_app2 con %#;
 fun if_rec  arg f y   = if is_rec arg then f (rec_of arg) else y;
 fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) Id (%# arg);
-fun prj _  _  y 1 _ = y
-|   prj f1 _  y _ 0 = f1 y
-|   prj f1 f2 y i j = prj f1 f2 (f2 y) (i-1) (j-1);
-val cproj    = prj (fn S => %%"cfst"`S) (fn S => %%"csnd"`S);
-val  proj    = prj (fn S => %%"fst" $S) (fn S => %%"snd" $S);
+fun prj _  _  x (   _::[]) _ = x
+|   prj f1 _  x (_::y::ys) 0 = f1 x y
+|   prj f1 f2 x (y::   ys) j = prj f1 f2 (f2 x y) ys (j-1);
+fun fix_tp (tn, args) = (tn, map (K oneT) args); (* instantiate type to
+						    avoid type varaibles *)
+val  proj        = prj (fn S => K(%%"fst" $S)) (fn S => K(%%"snd" $S));
+val cproj        = prj (fn S => K(%%"cfst"`S)) (fn S => K(%%"csnd"`S));
+fun cproj' T eqs = prj 
+	(fn S => fn t => Const("cfst",mk_prodT(dummyT,t)->>dummyT)`S) 
+	(fn S => fn t => Const("csnd",mk_prodT(t,dummyT)->>dummyT)`S) 
+		       T (map ((fn tp => tp ->> tp) o Type o fix_tp o fst) eqs);
 fun lift tfn = foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
 
 fun /\ v T = %%"fabs" $ mk_lam(v,T);