[isabelle] translations and numerals



I am using Library/Extended that defines a datatype with a unary constructor
Fin. I want to print terms like "Fin 5" as "5" and am using the following
translations:

translations
"_Numeral i" <= "CONST Fin(_Numeral i)"
"0" <= "CONST Fin 0"
"1" <= "CONST Fin 1"

When I generate latex from

text{* @{term "Fin(5::int)"} *}

this works fine, I get "5".

But when I write

term "Fin(5::int)"

in a theory, the output is "Fin 5". Why is that? And what can I do to obtain the
output "5" always, not just from an antiquotation in a text block.

Note that when I use this translation

translations
"x" <= "CONST Fin(x)"

then "Fin" disappears for good, but that is not what I want.

Thanks
Tobias




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