mk_comb : term * term -> term
STRUCTURE
Term
SYNOPSIS
Constructs a combination (function application).
DESCRIPTION
mk_comb (t1,t2) returns the combination t1 t2.
FAILURE
Fails if t1 does not have a function type, or if t1 has a function type, but its domain does not equal the type of t2.
EXAMPLE
   - mk_comb (neg_tm,T);

   > val it = `~T` : term

   - mk_comb(T, T) handle e => Raise e;

   Exception raised at Term.mk_comb:
   incompatible types

SEEALSO
dest_comb, is_comb, list_mk_comb, mk_var, mk_const, mk_abs
HOL  Kananaskis-14