src/HOLCF/domain/library.ML
changeset 1834 c780a4f39454
parent 1828 d022c10d2c08
child 2238 c72a23bbe762
equal deleted inserted replaced
1833:59f5256d8dd2 1834:c780a4f39454
   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;
   181 fun when_body cons funarg = let
   183 fun when_body cons funarg = let
   182 	fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
   184 	fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
   183 	|   one_fun n (_,args) = let
   185 	|   one_fun n (_,args) = let
   184 		val l2 = length args;
   186 		val l2 = length args;
   185 		fun idxs m arg = (if is_lazy arg then fn x=> %%"lift"`%%"ID"`x
   187 		fun idxs m arg = (if is_lazy arg then fn x=> %%"lift"`%%"ID"`x