--- a/src/ZF/Tools/datatype_package.ML Mon Oct 04 21:39:10 1999 +0200
+++ b/src/ZF/Tools/datatype_package.ML Mon Oct 04 21:39:36 1999 +0200
@@ -90,9 +90,9 @@
(*The empty tuple is 0*)
fun mk_tuple [] = Const("0",iT)
- | mk_tuple args = foldr1 (app Pr.pair) args;
+ | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args;
- fun mk_inject n k u = access_bal (ap Su.inl, ap Su.inr, u) n k;
+ fun mk_inject n k u = access_bal (fn t => Su.inl $ t, fn t => Su.inr $ t, u) n k;
val npart = length rec_names; (*number of mutually recursive parts*)
@@ -120,7 +120,7 @@
CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
Ind_Syntax.iT
free
- in fold_bal (app Su.elim) (map call_f case_list) end;
+ in fold_bal (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list) end;
(** Generating function variables for the case definition
Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
@@ -155,7 +155,7 @@
val case_tm = list_comb (case_const, case_args);
val case_def = Logic.mk_defpair
- (case_tm, fold_bal (app Su.elim) (map call_case case_lists));
+ (case_tm, fold_bal (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
(** Generating function variables for the recursor definition