Strange parsing in fresh quotes

[phlegmaticprogrammer]

Apparently the ProofScript interpreter happily executes

let x:'«val ∅»'
let x:'«= ∅»'

which should not even parse.

[phlegmaticprogrammer]

@Chattered I created the following ProofScript file:

theory issue78 extends \root

context
  let x:'«val ∅»'
  let x:'«= ∅»'

and parsing of that theory file comes back with an error as expected. Are you sure it parses for you?

[phlegmaticprogrammer]

Everything seems to work as expected.

[phlegmaticprogrammer]

There is a related bug though that will for example let the following code fail:

  let '«val x»'
  let '«= x»'

[phlegmaticprogrammer]

@Chattered I pushed a fix which should take care of the bug you discovered.