# HG changeset patch
# User wenzelm
# Date 939065976 -7200
# Node ID 8752253211ca1e8837d2854b1200a723fbe6a7c6
# Parent  6d7f9f30e6dfb7c4eb42ea8f0e6a7d9ae5537d11
tuned;

diff -r 6d7f9f30e6df -r 8752253211ca src/ZF/Tools/datatype_package.ML
--- 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