--- a/src/HOL/Typerep.thy Thu Feb 25 22:15:27 2010 +0100
+++ b/src/HOL/Typerep.thy Thu Feb 25 22:17:33 2010 +0100
@@ -25,15 +25,16 @@
fun typerep_tr (*"_TYPEREP"*) [ty] =
Syntax.const @{const_syntax typerep} $
(Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
- (Syntax.const "itself" $ ty)) (* FIXME @{type_syntax} *)
+ (Syntax.const @{type_syntax itself} $ ty))
| typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
*}
typed_print_translation {*
let
- fun typerep_tr' show_sorts (*"typerep"*) (* FIXME @{type_syntax} *)
- (Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) =
+ fun typerep_tr' show_sorts (*"typerep"*)
+ (Type (@{type_syntax fun}, [Type (@{type_syntax itself}, [T]), _]))
+ (Const (@{const_syntax TYPE}, _) :: ts) =
Term.list_comb
(Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
| typerep_tr' _ T ts = raise Match;