[isabelle-dev] Numeral_Type.thy

[Brian Huffman]

Quoting Makarius <makarius at sketis.net>:

> Above @{const_name UNIV} should be @{const_syntax UNIV} -- this
> corresponds to the CONST marker in the 'translations' specification.
>
> BTW, these markers are smart enough to handle both old and authentic
> syntax as expected.
>
> The former @{const_name UNIV} happened to coincide with @{const_syntax
> UNIV}, because the constant was both global and non-authentic.

Thanks; the fix worked, and I've checked it in.

It's too bad that there isn't a type distinction between  
@{const_syntax foo} and @{const_name foo}. If there was, then this bug  
could have been caught a lot sooner.

- Brian