[isabelle-dev] goals inserts facts into goal statement

[Andreas Lochbihler]

I am trying to replace some of my old usages of case goal_* with the new goals method. In 
the course, I encountered the problem that goal inserts the facts chained in as additional 
assumptions of my goals and also for the case bindings. This is unfortunate when I use 
goals sequenced after rule. Below is a prototypical example:

   lemma foo: "[| X; Y; X ==> Y; Y ==> X |] ==> True" by simp

   have "A" and "B"
   then (* chaining is required to instantiate the free variables in the theorem *)
   show True
   proof(rule foo)
     case goal_1
     ...
   next
     case goal_2
     ...

Now, when I replace (rule foo) with (rule foo, goals), the goals methods inserts the facts 
A and B into every subgoal and into the case bindings. Is there a canonical way to avoid this?

I can of course write

   apply(rule foo) proof goals

but this feels like going against the spirit of Isar. Why does goals have to insert 
chained facts at all?

Andreas

PS: I am using Isabelle/3444e0bf9261.