src/HOLCF/domain/axioms.ML
changeset 16842 5979c46853d1
parent 16778 2162c0de4673
child 17811 10ebcd7032c1
     1.1 --- a/src/HOLCF/domain/axioms.ML	Thu Jul 14 19:28:23 2005 +0200
     1.2 +++ b/src/HOLCF/domain/axioms.ML	Thu Jul 14 19:28:24 2005 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  				Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
     1.5  
     1.6    fun con_def outer recu m n (_,args) = let
     1.7 -     fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else Id)
     1.8 +     fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else I)
     1.9  			(if recu andalso is_rec arg then (cproj (Bound z) eqs
    1.10  				  (rec_of arg))`Bound(z-x) else Bound(z-x));
    1.11       fun parms [] = %%:ONE_N
    1.12 @@ -47,7 +47,7 @@
    1.13  
    1.14    val copy_def = ("copy_def", %%:(dname^"_copy") == /\"f" (dc_abs oo 
    1.15  	Library.foldl (op `) (%%:(dname^"_when") , 
    1.16 -	              mapn (con_def Id true (length cons)) 0 cons)));
    1.17 +	              mapn (con_def I true (length cons)) 0 cons)));
    1.18  
    1.19  (* -- definitions concerning the constructors, discriminators and selectors - *)
    1.20  
    1.21 @@ -75,7 +75,7 @@
    1.22  		 mk_cRep_CFun(%%:(dname^"_when"),map 
    1.23  			(fn (con',args) => if con'<>con then UU else
    1.24  			 foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
    1.25 -	in List.mapPartial Id (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
    1.26 +	in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
    1.27  
    1.28  
    1.29  (* ----- axiom and definitions concerning induction ------------------------- *)