[isabelle] Strange variable binding on obtains - long-goal format

Hi all,

referring to Isaballe 2011-1

I just encountered some (in my opinion strange) behavior of the obtains
long-goal format:

  assumes P
  obtains sym where "sym = w"
  thm that

  sym = (w\<Colon>('a \<times> 'a \<Rightarrow> bool) \<Rightarrow>
bool) \<Longrightarrow> thesis\<Colon>bool

That is, sym is recognized as a constant (Relation.sym) here, instead of
a bound variable, as I would expect.
Is there a workaround, i.e., can I use a name declared as a constant
somewhere in an obtains-goal?
Adding a "fixes sym" to the lemma results in a "duplicate fixed
variable" error.

If this behavior is intended, is there any reason for silently ignoring
the variable binding given by the user, not even issuing a warning?


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