[isabelle] rule_format and locales

I want to use a rule_format transformation for a lemma inside a locale, but it does not work:

If I have, for example:
 consts A :: 'a
            B :: 'a

 locale dummy
 lemma (in dummy) X[rule_format]: "ALL x . A x --> B x" sorry

the lemma will be:
> thm dummy.X
ALL x . A x --> B x [!]

but I expected something like
!! x . A x ==> B x
A ?x ==> B ?x
as I get when using rule_format outside a locale.

Can I use something similiar to rule_format that works inside a locale, or do I have to transform the lemmas "by hand" ?

Greetings and thanks for any hints
 Peter Lammich

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