src/Pure/Syntax/parser.ML
changeset 19346 c4c003abd830
parent 19305 5c16895d548b
child 19482 9f11af8f7ef9