src/Pure/Syntax/parser.ML
changeset 38273 d31a34569542
parent 37852 a902f158b4fc
child 38711 79d3cbfb4730