--- a/src/HOL/Typerep.thy Wed Apr 06 12:55:53 2011 +0200
+++ b/src/HOL/Typerep.thy Wed Apr 06 12:58:13 2011 +0200
@@ -36,7 +36,7 @@
(Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
(Const (@{const_syntax TYPE}, _) :: ts) =
Term.list_comb
- (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
+ (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ show_sorts T, ts)
| typerep_tr' _ T ts = raise Match;
in [(@{const_syntax typerep}, typerep_tr')] end
*}