No highlighting on free variables in lemmas due to prefix errors

[AlphonsedeV]

The error highlight fails to highlight unbound temporal variables if they are wrongly prefixed.

The following equality condition between i and j will not be highlighted :

lemma example:
"
All k #i.
Action(k) @ i ==> not(Ex #j. K(k) @ j & i = j)
"

Despite the fact that i and j are unbound because of the missing # prefix in the equality condition (the prefix being optional for the @ and < operators, those correctly do not generate highlighting).

Example source: (.txt for upload)
Brokenhighlight.spthy.txt