src/Pure/name.ML
changeset 56454 e9e82384e5a1
parent 55949 4766342e8376
child 56811 b66639331db5