src/Pure/Syntax/parser.ML
changeset 7400 fbd5582761e6
parent 6962 399643633529
child 7944 cc1930ad1a88