src/Pure/name.ML
changeset 33696 2c7c79ca6c23
parent 33547 edfc35dcfe31
child 34307 9074aa7d06e0