Tune parser for better error messages

When parsing equational proofs, a parse error in a term would sometimes
be hidden by the parser backtracking too much and giving a nonsensical
error message.

This patch tries to solve this by committing earlier to a certain parse
path.