src/Pure/Syntax/parser.ML
changeset 42268 01401287c3f7
parent 42226 cb650789f2f0
child 42282 4fa41e068ff0