src/Pure/Syntax/local_syntax.ML
changeset 42268 01401287c3f7
parent 42240 5a4d30cd47a7
child 42284 326f57825e1a