inst_goal : instantiation -> goal -> goal

SYNOPSIS: Apply higher-order instantiation to a goal.
DESCRIPTION: The call inst_goal i g where i is an instantiation (as returned by term_match for example), will perform the instantiation indicated by i in both assumptions and conclusion of the goal g.
FAILURE CONDITIONS: Should never fail on a valid instantiation.
COMMENTS: Probably only of specialist interest to those writing tactics from scratch.
SEE ALSO: compose_insts, instantiate, INSTANTIATE, INSTANTIATE_ALL, PART_MATCH, term_match.