[isabelle-dev] Numeral_Type.thy

[Makarius]

On Thu, 12 Mar 2009, Brian Huffman wrote:

> The typed print translation in Numeral_Type.thy, which prints "card 
> (UNIV :: 'a set)" as "CARD('a)", is broken.
> 
> I think it has something to do with the new properly-qualified name for 
> "UNIV" that was introduced recently.
> 
> Anyway, I'm not exactly sure what is going wrong or how to fix it. Does 
> anyone have an idea?

Here is the (old) source:

syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")

translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)"

typed_print_translation {*
let
  fun card_univ_tr' show_sorts _ [Const (@{const_name UNIV}, Type(_,[T,_]))] =
    Syntax.const "_type_card" $ Syntax.term_of_typ show_sorts T;
in [(@{const_syntax card}, card_univ_tr')]
end
*}


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.


	Makarius