equal
deleted
inserted
replaced
34 let |
34 let |
35 fun typerep_tr' show_sorts (*"typerep"*) |
35 fun typerep_tr' show_sorts (*"typerep"*) |
36 (Type (@{type_name fun}, [Type (@{type_name 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_Phases.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 |
42 *} |
42 *} |
43 |
43 |
44 setup {* |
44 setup {* |