# HG changeset patch
# User oheimb
# Date 835881857 -7200
# Node ID c780a4f39454bd3da4c658697ff1b56b9090998e
# Parent  59f5256d8dd2ab73c3b058411ad08d635487e983
re-added when_funs to library.ML

diff -r 59f5256d8dd2 -r c780a4f39454 src/HOLCF/domain/library.ML
--- 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
diff -r 59f5256d8dd2 -r c780a4f39454 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Thu Jun 27 15:19:50 1996 +0200
+++ b/src/HOLCF/domain/theorems.ML	Thu Jun 27 15:24:17 1996 +0200
@@ -187,8 +187,7 @@
 end;
 
 local 
-  fun bind_fun t = foldr mk_All ((if length cons = 1 then ["f"] 
-		  else mapn (fn n => K("f"^(string_of_int n))) 1 cons),t);
+  fun bind_fun t = foldr mk_All (when_funs cons,t);
   fun bound_fun i _ = Bound (length cons - i);
   val when_app  = foldl (op `) (%%(dname^"_when"), mapn bound_fun 1 cons);
   val when_appl = pg [ax_when_def] (bind_fun(mk_trp(when_app`%x_name ===