fixed bug in prj' function
authorhuffman
Thu Mar 31 02:44:46 2005 +0200 (2005-03-31 ago)
changeset 156381fb24e545f88
parent 15637 d2a06007ebfa
child 15639 99ed5113783b
fixed bug in prj' function
src/HOLCF/domain/library.ML
     1.1 --- a/src/HOLCF/domain/library.ML	Thu Mar 31 00:10:35 2005 +0200
     1.2 +++ b/src/HOLCF/domain/library.ML	Thu Mar 31 02:44:46 2005 +0200
     1.3 @@ -160,7 +160,7 @@
     1.4  fun cproj x      = prj (fn S => K(%%:"cfst"`S)) (fn S => K(%%:"csnd"`S)) x;
     1.5  fun prj' _  _  x (   _::[]) _ = x
     1.6  |   prj' f1 _  x (_::   ys) 0 = f1 x (foldr' mk_prodT ys)
     1.7 -|   prj' f1 f2 x (y::   ys) j = prj f1 f2 (f2 x y) ys (j-1);
     1.8 +|   prj' f1 f2 x (y::   ys) j = prj' f1 f2 (f2 x y) ys (j-1);
     1.9  fun cproj' T eqs = prj'
    1.10  	(fn S => fn t => Const("cfst",mk_prodT(dummyT,t)->>dummyT)`S)
    1.11  	(fn S => fn t => Const("csnd",mk_prodT(t,dummyT)->>dummyT)`S)