src/Pure/Syntax/syn_trans.ML
changeset 9619 6125cc9efc18
parent 8595 06874c5c3cfa
child 10572 b070825579b8