src/HOL/Typerep.thy
changeset 42247 12fe41a92cd5
parent 42245 29e3967550d5
child 43329 84472e198515
     1.1 --- a/src/HOL/Typerep.thy	Wed Apr 06 13:27:59 2011 +0200
     1.2 +++ b/src/HOL/Typerep.thy	Wed Apr 06 13:33:46 2011 +0200
     1.3 @@ -30,13 +30,13 @@
     1.4  in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
     1.5  *}
     1.6  
     1.7 -typed_print_translation {*
     1.8 +typed_print_translation (advanced) {*
     1.9  let
    1.10 -  fun typerep_tr' show_sorts (*"typerep"*)
    1.11 +  fun typerep_tr' ctxt (*"typerep"*)
    1.12            (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
    1.13            (Const (@{const_syntax TYPE}, _) :: ts) =
    1.14          Term.list_comb
    1.15 -          (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ show_sorts T, ts)
    1.16 +          (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts)
    1.17      | typerep_tr' _ T ts = raise Match;
    1.18  in [(@{const_syntax typerep}, typerep_tr')] end
    1.19  *}