src/Pure/Syntax/syntax_trans.ML
changeset 44698 0385292321a0
parent 44433 9fbee4aab115
child 45057 86c9b73158a8