src/Pure/name.ML
changeset 28815 80bb72a0f577
parent 28792 1d80cee865de
child 28821 78a6ed46ad04