src/Pure/Syntax/syn_trans.ML
changeset 9502 50ec59aff389
parent 8595 06874c5c3cfa
child 10572 b070825579b8