src/HOLCF/domain/library.ML
changeset 1834 c780a4f39454
parent 1828 d022c10d2c08
child 2238 c72a23bbe762
--- a/src/HOLCF/domain/library.ML	Thu Jun 27 15:19:50 1996 +0200
+++ b/src/HOLCF/domain/library.ML	Thu Jun 27 15:24:17 1996 +0200
@@ -178,6 +178,8 @@
 |   cont_eta_contract t    = t;
 
 fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n);
+fun when_funs cons = if length cons = 1 then ["f"] 
+                     else mapn (fn n => K("f"^(string_of_int n))) 1 cons;
 fun when_body cons funarg = let
 	fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
 	|   one_fun n (_,args) = let