src/HOL/Typerep.thy
changeset 35363 09489d8ffece
parent 35299 4f4d5bf4ea08
child 35430 df2862dc23a8
     1.1 --- a/src/HOL/Typerep.thy	Thu Feb 25 22:15:27 2010 +0100
     1.2 +++ b/src/HOL/Typerep.thy	Thu Feb 25 22:17:33 2010 +0100
     1.3 @@ -25,15 +25,16 @@
     1.4    fun typerep_tr (*"_TYPEREP"*) [ty] =
     1.5          Syntax.const @{const_syntax typerep} $
     1.6            (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
     1.7 -            (Syntax.const "itself" $ ty))  (* FIXME @{type_syntax} *)
     1.8 +            (Syntax.const @{type_syntax itself} $ ty))
     1.9      | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
    1.10  in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
    1.11  *}
    1.12  
    1.13  typed_print_translation {*
    1.14  let
    1.15 -  fun typerep_tr' show_sorts (*"typerep"*)  (* FIXME @{type_syntax} *)
    1.16 -          (Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) =
    1.17 +  fun typerep_tr' show_sorts (*"typerep"*)
    1.18 +          (Type (@{type_syntax fun}, [Type (@{type_syntax itself}, [T]), _]))
    1.19 +          (Const (@{const_syntax TYPE}, _) :: ts) =
    1.20          Term.list_comb
    1.21            (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
    1.22      | typerep_tr' _ T ts = raise Match;