src/HOL/Typerep.thy
changeset 56243 2e10a36b8d46
parent 52435 6646bb548c6b
child 58152 6fe60a9a5bad
     1.1 --- a/src/HOL/Typerep.thy	Fri Mar 21 12:14:33 2014 +0100
     1.2 +++ b/src/HOL/Typerep.thy	Fri Mar 21 12:34:50 2014 +0100
     1.3 @@ -24,7 +24,7 @@
     1.4    let
     1.5      fun typerep_tr (*"_TYPEREP"*) [ty] =
     1.6            Syntax.const @{const_syntax typerep} $
     1.7 -            (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
     1.8 +            (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax Pure.type} $
     1.9                (Syntax.const @{type_syntax itself} $ ty))
    1.10        | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
    1.11    in [(@{syntax_const "_TYPEREP"}, K typerep_tr)] end
    1.12 @@ -34,7 +34,7 @@
    1.13    let
    1.14      fun typerep_tr' ctxt (*"typerep"*)
    1.15              (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
    1.16 -            (Const (@{const_syntax TYPE}, _) :: ts) =
    1.17 +            (Const (@{const_syntax Pure.type}, _) :: ts) =
    1.18            Term.list_comb
    1.19              (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts)
    1.20        | typerep_tr' _ T ts = raise Match;