1.1 --- a/src/HOL/Typerep.thy	Thu Feb 11 22:55:16 2010 +0100
     1.2 +++ b/src/HOL/Typerep.thy	Thu Feb 11 23:00:22 2010 +0100
     1.3 @@ -17,22 +17,27 @@
     1.4  
     1.5  end
     1.6  
     1.7 -setup {*
     1.8 +syntax
     1.9 +  "_TYPEREP" :: "type => logic"  ("(1TYPEREP/(1'(_')))")
    1.10 +
    1.11 +parse_translation {*
    1.12  let
    1.13    fun typerep_tr (*"_TYPEREP"*) [ty] =
    1.14 -        Lexicon.const @{const_syntax typerep} $ (Lexicon.const "_constrain" $ Lexicon.const "TYPE" $
    1.15 -          (Lexicon.const "itself" $ ty))
    1.16 +        Syntax.const @{const_syntax typerep} $
    1.17 +          (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
    1.18 +            (Syntax.const "itself" $ ty))  (* FIXME @{type_syntax} *)
    1.19      | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
    1.20 -  fun typerep_tr' show_sorts (*"typerep"*)
    1.21 +in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
    1.22 +*}
    1.23 +
    1.24 +typed_print_translation {*
    1.25 +let
    1.26 +  fun typerep_tr' show_sorts (*"typerep"*)  (* FIXME @{type_syntax} *)
    1.27            (Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) =
    1.28 -        Term.list_comb (Lexicon.const "_TYPEREP" $ Syntax.term_of_typ show_sorts T, ts)
    1.29 +        Term.list_comb
    1.30 +          (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
    1.31      | typerep_tr' _ T ts = raise Match;
    1.32 -in
    1.33 -  Sign.add_syntax_i
    1.34 -    [("_TYPEREP", Simple_Syntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")]
    1.35 -  #> Sign.add_trfuns ([], [("_TYPEREP", typerep_tr)], [], [])
    1.36 -  #> Sign.add_trfunsT [(@{const_syntax typerep}, typerep_tr')]
    1.37 -end
    1.38 +in [(@{const_syntax typerep}, typerep_tr')] end
    1.39  *}
    1.40  
    1.41  setup {*