src/Pure/Syntax/syn_trans.ML
changeset 4962 e9217cb15b42
parent 4700 20ade76722d6
child 5084 a676ada3b380