src/Pure/Syntax/scan.ML
changeset 6109 82b50115564c
parent 5987 389d03e6e093