# HG changeset patch
# User huffman
# Date 1110498307 -3600
# Node ID 83c0bf275b0fa864fb7c20e442a7205aac11241a
# Parent  2de79f49385684d70a43dd03c5d480143031252a
fixed bug: domain package can now define three or more mutually recursive types simultaneously

diff -r 2de79f493856 -r 83c0bf275b0f src/HOLCF/domain/library.ML
--- a/src/HOLCF/domain/library.ML	Fri Mar 11 00:43:52 2005 +0100
+++ b/src/HOLCF/domain/library.ML	Fri Mar 11 00:45:07 2005 +0100
@@ -158,8 +158,11 @@
 						    avoid type varaibles *)
 fun  proj x      = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
 fun cproj x      = prj (fn S => K(%%:"cfst"`S)) (fn S => K(%%:"csnd"`S)) x;
-fun cproj' T eqs = prj 
-	(fn S => fn t => Const("cfst",mk_prodT(dummyT,t)->>dummyT)`S) 
+fun prj' _  _  x (   _::[]) _ = x
+|   prj' f1 _  x (_::   ys) 0 = f1 x (foldr' mk_prodT ys)
+|   prj' f1 f2 x (y::   ys) j = prj f1 f2 (f2 x y) ys (j-1);
+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 = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));