mk_goalstate : goal -> goalstate

SYNOPSIS: Converts a goal into a 1-element goalstate.
DESCRIPTION: Given a goal g, the call mk_goalstate g converts it into a goalstate with that goal as its only member. (A goalstate consists of a list of subgoals as well as justification and metavariable information.)
FAILURE CONDITIONS: Never fails.
SEE ALSO: g, set_goal, TAC_PROOF.