using types one = unit lift and translations causes troubles between
authorslotosch
Mon Feb 17 11:01:10 1997 +0100 (1997-02-17)
changeset 2641533a84b3bedd
parent 2640 ee4dfce170a0
child 2642 3c3a84cc85a9
using types one = unit lift and translations causes troubles between
the type one and the constant one. The later was changed to ONE
src/HOLCF/domain/axioms.ML
     1.1 --- a/src/HOLCF/domain/axioms.ML	Mon Feb 17 10:57:11 1997 +0100
     1.2 +++ b/src/HOLCF/domain/axioms.ML	Mon Feb 17 11:01:10 1997 +0100
     1.3 @@ -38,7 +38,7 @@
     1.4       fun idxs z x arg = (if is_lazy arg then fn t => %%"up"`t else Id)
     1.5  			(if recu andalso is_rec arg then (cproj (Bound z) 
     1.6  			(length eqs) (rec_of arg))`Bound(z-x) else Bound(z-x));
     1.7 -     fun parms [] = %%"one"
     1.8 +     fun parms [] = %%"ONE"
     1.9       |   parms vs = foldr'(fn(x,t)=> %%"spair"`x`t)(mapn (idxs(length vs))1 vs);
    1.10       fun inj y 1 _ = y
    1.11       |   inj y _ 0 = %%"sinl"`y