semantic highlighting in dependent match

Stream: lean4

[Horațiu Cheval]

Using the default dark VSCode theme (which seems to be among those with the best support for Lean semantic highlighting),
in the definition of f below, p_ok is correctly colored as a variable, while p_wrong is highlighted as a constant.

inductive Formula where
| imp : Formula → Formula → Formula

inductive Proof : Formula → Type where
| mp {p q} : Proof p → Proof (.imp p q) → Proof q

def f {p} : Proof p → Int
| @Proof.mp p_ok p_wrong h₁ h₂ => sorry

It looks like this on my install.
image.png

Is this a known issue? (if indeed an issue)