src/Pure/Syntax/syn_trans.ML
changeset 10271 45b996639c45
parent 8595 06874c5c3cfa
child 10572 b070825579b8