src/Pure/Syntax/local_syntax.ML
changeset 81954 6f2bcdfa9a19
parent 81594 7e1b66416b7f