Unfortunately that was not visible on the isabelle-users mailing list. As far as I can tell (from looking at the development version of Isabelle), the next Isabelle release will behave as expected on your example, i.e., the result will be:
Makarius has already fixed this in the development branch, your example works there. This will also work in the next Isabelle release as expected. For the moment, you cannot do much about this in Isabelle2012. If you absolutely depend on this working correct, you could try and switch to the development version, but this incurs a lot of extra trouble.
> Nesting two contexts, where the inner context makes assumptions about
> fixed variables from the outer context, results in unexpected
> all-quantified assumptions. Consider this minimal example:
> fixes I :: "'a set"
> assumes I: "finite I"
> lemma test: "something_about I"
> Looking at the fact `test` from outside both contexts with `thm test`, I
> (!!I. finite I) ==> ?something_about ?I
> Obviously, this fact says something completely different. Am I doing
> something wrong here?
-- Karlsruher Institut f r Technologie
Dr. Andreas Lochbihler
Am Fasanengarten 5, Geb. 50.34, Raum 025
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
http://pp.info.uni-karlsruhe.de KIT - Universit t des Landes Baden-W rttemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft