Case expression prints badly

[mn200]

The definition

Definition a_def:
  a x =
  case x of
  | y::ys => if y = T then SOME y else SOME F
  | [] => NONE
End

parses correctly, but prints as

val a_def =
   ⊢ ∀x. a x = case x of [] => NONE | T::ys => SOME y | y::ys => SOME F: thm

where the y in the second clause is printed as a free variable (just as it appears), even though it’s actually the y of the first branch of the definition, and thus bound.

[mn200]

Thanks to Arve Gengelbach for the bug report.