src/Pure/Syntax/parser.ML
changeset 6942 f291292d727c
parent 6844 3909657a7da6
child 6962 399643633529