src/Pure/Syntax/syntax_trans.ML
changeset 43328 10d731b06ed7
parent 43326 47cf4bc789aa
child 44241 7943b69f0188