src/Pure/Syntax/parser.ML
changeset 43868 9684251c7ec1
parent 42374 b9a6b465da25
child 44102 954e9d6782ea