eliminated ap/app;
authorwenzelm
Mon Oct 04 21:46:13 1999 +0200 (1999-10-04)
changeset 77049a6783fdb9a5
parent 7703 6b3424e877bd
child 7705 222b715b5d24
eliminated ap/app;
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Mon Oct 04 21:45:10 1999 +0200
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Mon Oct 04 21:46:13 1999 +0200
     1.3 @@ -427,14 +427,14 @@
     1.4      val def_names = map (fn i => big_size_name ^ "_def_" ^ string_of_int i)
     1.5        (1 upto length recTs);
     1.6  
     1.7 -    val plus_t = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT);
     1.8 +    fun plus (t1, t2) = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
     1.9  
    1.10      fun make_sizefun (_, cargs) =
    1.11        let
    1.12          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    1.13          val k = length (filter is_rec_type cargs);
    1.14          val t = if k = 0 then HOLogic.zero else
    1.15 -          foldl1 (app plus_t) (map Bound (k - 1 downto 0) @ [HOLogic.mk_nat 1])
    1.16 +          foldl1 plus (map Bound (k - 1 downto 0) @ [HOLogic.mk_nat 1])
    1.17        in
    1.18          foldr (fn (T, t') => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT, t)
    1.19        end;
     2.1 --- a/src/HOL/Tools/datatype_prop.ML	Mon Oct 04 21:45:10 1999 +0200
     2.2 +++ b/src/HOL/Tools/datatype_prop.ML	Mon Oct 04 21:46:13 1999 +0200
     2.3 @@ -224,7 +224,7 @@
     2.4  
     2.5        in (ts @ [HOLogic.mk_Trueprop (HOLogic.mk_eq
     2.6          (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
     2.7 -         list_comb (f, frees @ (map (uncurry ap) (reccombs' ~~ frees')))))], fs)
     2.8 +         list_comb (f, frees @ (map (op $) (reccombs' ~~ frees')))))], fs)
     2.9        end
    2.10  
    2.11    in fst (foldl (fn (x, ((dt, T), comb_t)) =>
    2.12 @@ -408,7 +408,7 @@
    2.13      val size_consts = map (fn (s, T) =>
    2.14        Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
    2.15  
    2.16 -    val plus_t = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT);
    2.17 +    fun plus (t1, t2) = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;
    2.18  
    2.19      fun make_size_eqn size_const T (cname, cargs) =
    2.20        let
    2.21 @@ -420,7 +420,7 @@
    2.22          val ts = map (fn ((r, s), T) => nth_elem (dest_DtRec r, size_consts) $
    2.23            Free (s, T)) (recs ~~ rec_tnames ~~ recTs);
    2.24          val t = if ts = [] then HOLogic.zero else
    2.25 -          foldl1 (app plus_t) (ts @ [HOLogic.mk_nat 1])
    2.26 +          foldl1 plus (ts @ [HOLogic.mk_nat 1])
    2.27        in
    2.28          HOLogic.mk_Trueprop (HOLogic.mk_eq (size_const $
    2.29            list_comb (Const (cname, Ts ---> T), map Free (tnames ~~ Ts)), t))
     3.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Oct 04 21:45:10 1999 +0200
     3.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Mon Oct 04 21:46:13 1999 +0200
     3.3 @@ -110,7 +110,7 @@
     3.4  
     3.5      (* make injections for constructors *)
     3.6  
     3.7 -    fun mk_univ_inj ts = access_bal (ap In0, ap In1, if ts = [] then
     3.8 +    fun mk_univ_inj ts = access_bal (fn t => In0 $ t, fn t => In1 $ t, if ts = [] then
     3.9          Const ("arbitrary", Univ_elT)
    3.10        else
    3.11          foldr1 (HOLogic.mk_binop Scons_name) ts);