[isabelle-dev] Error highlighting in ML for @{lemma}

[Lars Noschinski]

Hi,

If I insert a lemma antiquotation in ML code with a proposition with a
type error, the error message is not attached to the proposition or the
antiquotation but to the whole block or file of ML. This refers to
13b06c6261.

  -- Lars