src/Pure/Syntax/syntax_phases.ML
changeset 80945 584828fa7a97
parent 80882 2cdb00f797b1
child 80950 b4a6bee4621a