[isabelle] term notation affects type parsing



Dear all,

when I declare syntax for a constant that coincides with the name of a type constructor, Isabelle afterwards cannot parse the type name any more. Here's an example:

typedecl mytype
consts foo :: "nat => nat"
notation foo ("mytype")
typ "mytype" (* fails with:

*** Inner syntax error at "mytype"
*** Failed to parse type
*** At command "typ"
*)

Why is this? I would have expected term and type syntax to be strictly separated syntactic categories. Is there a mode on which I can restrict notation such that it does not mess up type parsing?

Surprisingly, parsing works again if I add the following type_notation:

type_notation mytype ("mytype")
typ "mytype"
term "mytype"

Can I avoid the extra syntax notation for the type?

By the way, I used the RC1 of Isabelle2011-1.

Thanks for any help in advance,
Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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