| changeset 56205 | ceb8a93460b7 |
| parent 56069 | 451d5b73f8cf |
| child 56208 | 06cc31dff138 |
| 56204:f70e69208a8c | 56205:ceb8a93460b7 |
|---|---|
352 |
352 |
353 |
353 |
354 (** Isar setup **) |
354 (** Isar setup **) |
355 |
355 |
356 val _ = |
356 val _ = |
357 Theory.setup (ML_Context.antiquotation @{binding code} Args.term (fn _ => ml_code_antiq)); |
357 Theory.setup (ML_Antiquotation.declaration @{binding code} Args.term (fn _ => ml_code_antiq)); |
358 |
358 |
359 local |
359 local |
360 |
360 |
361 val parse_datatype = |
361 val parse_datatype = |
362 Parse.name --| @{keyword "="} -- |
362 Parse.name --| @{keyword "="} -- |