Fix scope/matching issues in proof scripts

Need to treat appeals to tactics as independent calls to the elaborator,
with known current scope, so don't add implicits until just before
invoking the tactic, and add a final unify/match step to collect any
missing implicits.