Delay evaluation of theorem-producing function till needed.
DESCRIPTION
Given a theorem-producing inference rule f and its argument a, the tactic
RECALL_ACCEPT_TAC f a will evaluate th = f a and do ACCEPT_TAC th, but
only when the tactic is applied to a goal.
FAILURE CONDITIONS
Never fails until subsequently applied to a goal, but then may fail if the
theorem-producing function does.