--- 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 ===