equal
deleted
inserted
replaced
31 *} |
31 *} |
32 |
32 |
33 typed_print_translation {* |
33 typed_print_translation {* |
34 let |
34 let |
35 fun typerep_tr' show_sorts (*"typerep"*) |
35 fun typerep_tr' show_sorts (*"typerep"*) |
36 (Type (@{type_syntax fun}, [Type (@{type_syntax itself}, [T]), _])) |
36 (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _])) |
37 (Const (@{const_syntax TYPE}, _) :: ts) = |
37 (Const (@{const_syntax TYPE}, _) :: ts) = |
38 Term.list_comb |
38 Term.list_comb |
39 (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts) |
39 (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts) |
40 | typerep_tr' _ T ts = raise Match; |
40 | typerep_tr' _ T ts = raise Match; |
41 in [(@{const_syntax typerep}, typerep_tr')] end |
41 in [(@{const_syntax typerep}, typerep_tr')] end |