--- a/src/HOL/Library/Phantom_Type.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Library/Phantom_Type.thy Sat May 25 15:37:53 2013 +0200
@@ -27,13 +27,13 @@
translations
"Phantom('t)" => "CONST phantom :: _ \<Rightarrow> ('t, _) phantom"
-typed_print_translation (advanced) {*
-let
- fun phantom_tr' ctxt
- (Type (@{type_name fun}, [_, Type (@{type_name phantom}, [T, _])])) ts =
- Term.list_comb (Syntax.const @{syntax_const "_Phantom"} $ Syntax_Phases.term_of_typ ctxt T, ts)
- | phantom_tr' _ _ _ = raise Match;
-in [(@{const_syntax phantom}, phantom_tr')] end
+typed_print_translation {*
+ let
+ fun phantom_tr' ctxt
+ (Type (@{type_name fun}, [_, Type (@{type_name phantom}, [T, _])])) ts =
+ list_comb (Syntax.const @{syntax_const "_Phantom"} $ Syntax_Phases.term_of_typ ctxt T, ts)
+ | phantom_tr' _ _ _ = raise Match;
+ in [(@{const_syntax phantom}, phantom_tr')] end
*}
end