mk_icomb : term * term -> term

SYNOPSIS
Makes a combination, instantiating types in rator if necessary.

DESCRIPTION
The call mk_icomb(f,x) makes the combination f x, just as with mk_comb, but if necessary to ensure the types are compatible it will instantiate type variables in f first.

FAILURE CONDITIONS
Fails if the rator type is impossible to instantiate compatibly.

EXAMPLE
The analogous call to the following using plain mk_const would fail:
  # mk_icomb(`(!)`,`\x. x = 1`);;
  Warning: inventing type variables
  val it : term = `!x. x = 1`

USES
A handy way of making combinations involving polymorphic constants, without needing a manual instantiation of the generic type.

SEE ALSO
list_mk_icomb, mk_comb, type_match.