| changeset 52143 | 36ffe23b25f8 |
| parent 42284 | 326f57825e1a |
| child 53241 | effd8fcabca2 |
| 52142:348aed032cda | 52143:36ffe23b25f8 |
|---|---|
16 |
16 |
17 parse_translation {* |
17 parse_translation {* |
18 let |
18 let |
19 fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t |
19 fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t |
20 | quote_tr ts = raise TERM ("quote_tr", ts); |
20 | quote_tr ts = raise TERM ("quote_tr", ts); |
21 in [(@{syntax_const "_quote"}, quote_tr)] end |
21 in [(@{syntax_const "_quote"}, K quote_tr)] end |
22 *} |
22 *} |
23 |
23 |
24 end |
24 end |