src/HOLCF/domain/library.ML
changeset 1828 d022c10d2c08
parent 1819 245721624c8d
child 1834 c780a4f39454
equal deleted inserted replaced
1827:724e7d8990ea 1828:d022c10d2c08
   176       | body' => Const("fabs",TT) $ Abs(a,T,body'))
   176       | body' => Const("fabs",TT) $ Abs(a,T,body'))
   177 |   cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t
   177 |   cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t
   178 |   cont_eta_contract t    = t;
   178 |   cont_eta_contract t    = t;
   179 
   179 
   180 fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n);
   180 fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n);
   181 fun when_funs cons = if length cons = 1 then ["f"] 
       
   182 		     else mapn (fn n => K("f"^(string_of_int n))) 1 cons;
       
   183 fun when_body cons funarg = let
   181 fun when_body cons funarg = let
   184 	fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
   182 	fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
   185 	|   one_fun n (_,args) = let
   183 	|   one_fun n (_,args) = let
   186 		val l2 = length args;
   184 		val l2 = length args;
   187 		fun idxs m arg = (if is_lazy arg then fn x=> %%"lift"`%%"ID"`x
   185 		fun idxs m arg = (if is_lazy arg then fn x=> %%"lift"`%%"ID"`x