src/Pure/Syntax/parser.ML
changeset 1072 0140ff702b23
parent 890 2b7275b13bef
child 1147 57b5f55bf879