[isabelle-dev] Bad theory import "Main"

[Blanchette, J.C.]

Hi Makarius,

> The problem is in the HOL-Lib session from isafor. It is somewhere in
> your ROOTS (or -d specifications).

Ah!

> Are you working with IsaFoR on purpose, or is this just an accident?

That's it. I had IsaFoR as a component -- half on purpose, half by accident.

Thanks for helping me debug it.

> In current Isabelle/6acb28e5ba41 it is also possible to use something
> like "isabelle jedit -R -l MY_SESSION" to restrict the theory name space
> to the requirements of MY_SESSION.

Good to know.

Jasmin