src/Pure/Syntax/parser.ML
changeset 17249 e89fbfd778c1
parent 17221 6cd180204582
child 17314 04e21a27c0ad