tuned;
authorwenzelm
Sat May 25 17:40:44 2013 +0200 (2013-05-25)
changeset 521479943f8067f11
parent 52146 ceb31e1ded30
child 52148 893b15200ec1
tuned;
src/HOL/Library/Cardinality.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/Phantom_Type.thy
     1.1 --- a/src/HOL/Library/Cardinality.thy	Sat May 25 17:13:34 2013 +0200
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Sat May 25 17:40:44 2013 +0200
     1.3 @@ -43,9 +43,9 @@
     1.4  
     1.5  translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
     1.6  
     1.7 -typed_print_translation {*
     1.8 +print_translation {*
     1.9    let
    1.10 -    fun card_univ_tr' ctxt _ [Const (@{const_syntax UNIV}, Type (_, [T]))] =
    1.11 +    fun card_univ_tr' ctxt [Const (@{const_syntax UNIV}, Type (_, [T]))] =
    1.12        Syntax.const @{syntax_const "_type_card"} $ Syntax_Phases.term_of_typ ctxt T
    1.13    in [(@{const_syntax card}, card_univ_tr')] end
    1.14  *}
     2.1 --- a/src/HOL/Library/Numeral_Type.thy	Sat May 25 17:13:34 2013 +0200
     2.2 +++ b/src/HOL/Library/Numeral_Type.thy	Sat May 25 17:40:44 2013 +0200
     2.3 @@ -519,7 +519,8 @@
     2.4        | bit_tr' b _ = raise Match;
     2.5    in
     2.6     [(@{type_syntax bit0}, K (bit_tr' 0)),
     2.7 -    (@{type_syntax bit1}, K (bit_tr' 1))] end;
     2.8 +    (@{type_syntax bit1}, K (bit_tr' 1))]
     2.9 +  end;
    2.10  *}
    2.11  
    2.12  subsection {* Examples *}
     3.1 --- a/src/HOL/Library/Phantom_Type.thy	Sat May 25 17:13:34 2013 +0200
     3.2 +++ b/src/HOL/Library/Phantom_Type.thy	Sat May 25 17:40:44 2013 +0200
     3.3 @@ -29,10 +29,10 @@
     3.4  
     3.5  typed_print_translation {*
     3.6    let
     3.7 -    fun phantom_tr' ctxt 
     3.8 -        (Type (@{type_name fun}, [_, Type (@{type_name phantom}, [T, _])])) ts =
     3.9 -          list_comb (Syntax.const @{syntax_const "_Phantom"} $ Syntax_Phases.term_of_typ ctxt T, ts)
    3.10 -    | phantom_tr' _ _ _ = raise Match;
    3.11 +    fun phantom_tr' ctxt (Type (@{type_name fun}, [_, Type (@{type_name phantom}, [T, _])])) ts =
    3.12 +          list_comb
    3.13 +            (Syntax.const @{syntax_const "_Phantom"} $ Syntax_Phases.term_of_typ ctxt T, ts)
    3.14 +      | phantom_tr' _ _ _ = raise Match;
    3.15    in [(@{const_syntax phantom}, phantom_tr')] end
    3.16  *}
    3.17