[isabelle] [symmetric]-attribute changes variable names

Hi all,

I recently stumbled over the following quite confusing behaviour:

definition "foo x \<equiv> x"
thm foo_def[symmetric]
  > Outputs ?y = foo ?y

Is it really necessary that symmetric is allowed to change variable
names in the theorem? For a user, it may be quite confusing having to
  foo[where x="bar"], but foo[symmetric, where y="bar"]

-- Peter

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