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.