[isabelle-dev] "interpret ... for a" leaks a

[Lars Noschinski]

Hi,

in 40fe6b80b481, I stumbled upon the following behaviour. Consider
the following example:

   locale Foo = fixes a :: 'a

   notepad begin
     interpret Foo b for b .
     term b
   end

jEdit tells me about b in the term command:

   term
   fixed "b"
   skolem variable
   :: 'b

So the b from the "for b" is leaked into the surrounding context. As all 
the lemmas about b where generalized, I would have expected that
b does not become fixed in the surrounding context.

   -- Lars