author oheimb Thu, 27 Jun 1996 15:24:17 +0200 changeset 1834 c780a4f39454 parent 1833 59f5256d8dd2 child 1835 07eee14f5bd4
 src/HOLCF/domain/library.ML file | annotate | diff | comparison | revisions src/HOLCF/domain/theorems.ML file | annotate | diff | comparison | revisions
```--- 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```
```--- 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 ===```