The following example produces an error:

Theorem test:
  (λ(x,_). x) y = foo a
Proof
  pairarg_tac >>
  qpat_abbrev_tac ‘bar = foo _’ >>
  cheat
QED

This is related to ba1eb9a (and 7b64934 linked in the commit message). In particular:

• the underscore used as a bound variable becomes _0
• pairarg_tac brings free variable _0 into scope
• parsing of qpat_abbrev_tac fails as it names its input underscore as _0 too, which clashes with the one free in the goal
  This causes a type conflict.

Discussion with @mn200 and @konrad-slind on Zulip suggests that this is an issue in qpat_abbrev_tac, which is failing to account for the new handing of underscores.