equal
deleted
inserted
replaced
14 translations |
14 translations |
15 ".{b}." \<rightharpoonup> "CONST Collect \<guillemotleft>b\<guillemotright>" |
15 ".{b}." \<rightharpoonup> "CONST Collect \<guillemotleft>b\<guillemotright>" |
16 |
16 |
17 parse_translation {* |
17 parse_translation {* |
18 let |
18 let |
19 fun quote_tr [t] = Syntax.quote_tr "_antiquote" t |
19 fun quote_tr [t] = Syntax.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 [("_quote", quote_tr)] end |
21 in [(@{syntax_const "_quote"}, quote_tr)] end |
22 *} |
22 *} |
23 |
23 |
24 end |
24 end |