# [isabelle] Unexpected assumptions in nested contexts

(I already posted this several months ago, got no replies, and forgot
about it. I'm sending it again in case there's a solution/workaround
which I've missed. The original thread is at
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-June/msg00052.html>.)
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:
context
fixes I :: "'a set"
begin
context
assumes I: "finite I"
begin
lemma test: "something_about I"
sorry
end
end
Looking at the fact `test` from outside both contexts with `thm test`, I
get:
(!!I. finite I) ==> ?something_about ?I
Obviously, this fact says something completely different. Am I doing
something wrong here?

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*