The parser seems to be too restrictive for patterns when defining local ghost values by let ghost PATTERN = EXPR in EXPR. Each of the lines marked with a-c are refused with error "illegal ghost qualifier":

let constant u : unit =
  let e = (0, 0) in
  let ghost _ = e in (* a *)
  let ghost _, y = e in (* b *)
  let ghost (x, y) = e in (* c *)
  ()

But the lines marked with e-g are accepted.

let constant u : unit =
  let e = (0, 0) in
  let ghost _x = e in (* e *)
  let ghost _x, y = e in (* f *)
  let ghost x, y = e in (* g *)
  ()

I would expect all lines a-g syntactically valid in Why3 (as they were in version 0.88).