src/Pure/name.ML
changeset 73408 be11fe268b33
parent 69137 90fce429e1bc
child 74411 20b0b27bc6c7