[isabelle-dev] Commands not in scope fail to cause errors

[Jasmin Blanchette]

> On 10.04.2015, at 09:03, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
> Something similar happens under 364b0512ce74 if the theory starts with a section command followed by a lemma before the actual theory.

I observed something similar in a somewhat different scenario earlier this week. I was working on a theory called “Foo.thy” that introduced the “foo” keyword. At one point, I accidentally tried to use “foo” before it was actually introduced (by an “ML_file” command a few lines below).

Jasmin