# [isabelle] Interpretation problems of locales with datatype declarations

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] Interpretation problems of locales with datatype declarations
*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
*Date*: Tue, 3 Nov 2015 10:52:18 +0100
*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

Dear BNF experts,

`I have started to use datatype declarations inside locales, but this seems to cause
``problems at interpretations. Here is an example:
`
locale l = fixes n :: nat begin
datatype 'a foo = Foo 'a
end
interpretation l 0 .
The interpretation raises
exception THM 0 raised (line 1216 of "thm.ML"):
Type not of sort term_of
term_of_class.term_of ?x â ?t

`If the interpretation is inside a proof (rather than at the top-level), interpret works
``once, but I get a different error upon the second interpretation:
`
locale l2 = fixes b :: bool begin
datatype 'b bar = Bar | Foobar 'b
lemma True
proof -
interpret t!: l2 True .
oops
end
Here, interpret complains that
Monotocity rule for type "Scratch.l2.bar" is already_defined.

`Is this a fundamental problem of the BNF package and locales or just a limitation of the
``current implementation? Can I disable some plugins to make the examples work?
`
Best,
Andreas

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