# [isabelle] Converting fixed variables to ?-wildcards

Assume I have some lemma in a locale
locale test = fixes A::"'a list set"
assumes [...]
begin
[...]
lemma test[simp]: "a at b\<in>A <--> a\<in>A & b\<in>A"

`in order to apply this lemma also to lists of the form "a#as", outside a
``locale, I would usually do
` lemmas test'[simp] = test[of "[x]", simplified, standard]

`the problem is, that standard does not only convert the fixed variable x
``to a wildcard variable ?x, but it also prefixes the lemma with an
``assumption "test A", because we are inside the locale. Instead of the
``desired
` "?x#?b\<in>A <--> [?x]\<in>A & b\<in>A",
I get
"test A ==> ?x#?b\<in>A <--> [?x]\<in>A & b\<in>A"

`and this lemma won't work as a simplification rule inside the locale
``context.
`

`Is there a way to the fixed variables replaced by wildcards, but not
``getting this locale-assumption in front of the lemma (of course, without
``retyping and proving the special version of the lemma ;) ) ?
`
Regards,
Peter

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