src/Pure/Syntax/syn_trans.ML
changeset 4030 ca44afcc259c
parent 3928 787d2659ce4a
child 4148 e0e5a2820ac1