equal
deleted
inserted
replaced
25 |
25 |
26 syntax "_Phantom" :: "type \<Rightarrow> logic" ("(1Phantom/(1'(_')))") |
26 syntax "_Phantom" :: "type \<Rightarrow> logic" ("(1Phantom/(1'(_')))") |
27 translations |
27 translations |
28 "Phantom('t)" => "CONST phantom :: _ \<Rightarrow> ('t, _) phantom" |
28 "Phantom('t)" => "CONST phantom :: _ \<Rightarrow> ('t, _) phantom" |
29 |
29 |
30 typed_print_translation (advanced) {* |
30 typed_print_translation {* |
31 let |
31 let |
32 fun phantom_tr' ctxt |
32 fun phantom_tr' ctxt |
33 (Type (@{type_name fun}, [_, Type (@{type_name phantom}, [T, _])])) ts = |
33 (Type (@{type_name fun}, [_, Type (@{type_name phantom}, [T, _])])) ts = |
34 Term.list_comb (Syntax.const @{syntax_const "_Phantom"} $ Syntax_Phases.term_of_typ ctxt T, ts) |
34 list_comb (Syntax.const @{syntax_const "_Phantom"} $ Syntax_Phases.term_of_typ ctxt T, ts) |
35 | phantom_tr' _ _ _ = raise Match; |
35 | phantom_tr' _ _ _ = raise Match; |
36 in [(@{const_syntax phantom}, phantom_tr')] end |
36 in [(@{const_syntax phantom}, phantom_tr')] end |
37 *} |
37 *} |
38 |
38 |
39 end |
39 end |