src/HOL/Typerep.thy
changeset 42245 29e3967550d5
parent 38857 97775f3e8722
child 42247 12fe41a92cd5
     1.1 --- a/src/HOL/Typerep.thy	Wed Apr 06 12:55:53 2011 +0200
     1.2 +++ b/src/HOL/Typerep.thy	Wed Apr 06 12:58:13 2011 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4            (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
     1.5            (Const (@{const_syntax TYPE}, _) :: ts) =
     1.6          Term.list_comb
     1.7 -          (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
     1.8 +          (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ show_sorts T, ts)
     1.9      | typerep_tr' _ T ts = raise Match;
    1.10  in [(@{const_syntax typerep}, typerep_tr')] end
    1.11  *}