eliminated ap/app;

--- a/src/HOL/Tools/datatype_abs_proofs.ML	Mon Oct 04 21:45:10 1999 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Mon Oct 04 21:46:13 1999 +0200
@@ -427,14 +427,14 @@
     val def_names = map (fn i => big_size_name ^ "_def_" ^ string_of_int i)
       (1 upto length recTs);
 
-    val plus_t = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT);
+    fun plus (t1, t2) = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
 
     fun make_sizefun (_, cargs) =
       let
         val Ts = map (typ_of_dtyp descr' sorts) cargs;
         val k = length (filter is_rec_type cargs);
         val t = if k = 0 then HOLogic.zero else
-          foldl1 (app plus_t) (map Bound (k - 1 downto 0) @ [HOLogic.mk_nat 1])
+          foldl1 plus (map Bound (k - 1 downto 0) @ [HOLogic.mk_nat 1])
       in
         foldr (fn (T, t') => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT, t)
       end;

--- a/src/HOL/Tools/datatype_prop.ML	Mon Oct 04 21:45:10 1999 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Mon Oct 04 21:46:13 1999 +0200
@@ -224,7 +224,7 @@
 
       in (ts @ [HOLogic.mk_Trueprop (HOLogic.mk_eq
         (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
-         list_comb (f, frees @ (map (uncurry ap) (reccombs' ~~ frees')))))], fs)
+         list_comb (f, frees @ (map (op $) (reccombs' ~~ frees')))))], fs)
       end
 
   in fst (foldl (fn (x, ((dt, T), comb_t)) =>
@@ -408,7 +408,7 @@
     val size_consts = map (fn (s, T) =>
       Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
 
-    val plus_t = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT);
+    fun plus (t1, t2) = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
 
     fun make_size_eqn size_const T (cname, cargs) =
       let
@@ -420,7 +420,7 @@
         val ts = map (fn ((r, s), T) => nth_elem (dest_DtRec r, size_consts) $
           Free (s, T)) (recs ~~ rec_tnames ~~ recTs);
         val t = if ts = [] then HOLogic.zero else
-          foldl1 (app plus_t) (ts @ [HOLogic.mk_nat 1])
+          foldl1 plus (ts @ [HOLogic.mk_nat 1])
       in
         HOLogic.mk_Trueprop (HOLogic.mk_eq (size_const $
           list_comb (Const (cname, Ts ---> T), map Free (tnames ~~ Ts)), t))

--- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Oct 04 21:45:10 1999 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Mon Oct 04 21:46:13 1999 +0200
@@ -110,7 +110,7 @@
 
     (* make injections for constructors *)
 
-    fun mk_univ_inj ts = access_bal (ap In0, ap In1, if ts = [] then
+    fun mk_univ_inj ts = access_bal (fn t => In0 $ t, fn t => In1 $ t, if ts = [] then
         Const ("arbitrary", Univ_elT)
       else
         foldr1 (HOLogic.mk_binop Scons_name) ts);