# [isabelle] obtains forgets consumes and case_names in locales

Hi all,
I stumbled across the following odd behaviour of obtains in locales:

`Normally, theorems stated with obtains carry appropriate case_names and
``consumes declaration, e.g. the following works as expected.
`
lemma test:
assumes "n = n"
obtains (first_case) "n = 0"
| (second_case) n' where "n = Suc n'"
by(cases n) auto
lemma assumes "n = n" shows P
using assms
proof(cases rule: test)
case first_case
next
case (second_case n')
oops

`When I do not provide names for the obtains-cases in the lemma, test is
``still declared with a "consumes 1" and case_names 1 2.
`

`However, when I put lemma test into a locale that fixes at least one
``parameter, these declarations change:
`
locale A =
fixes a :: "'a"
begin
lemma test:
assumes "n = n"
obtains (first_case) "n = 0"
| (second_case) n' where "n = Suc n'"
by(cases n) auto

`Lemma test now carries the consumes 0 declaration and case_names 1 2 3,
``independent of whether the names for obtains-cases are given - which is
``at least unexpected.
``Is this a bug or am I better not to rely on obtains producing proper
``consumes and case_names declarations in general?
`
Regards,
Andreas

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