src/Pure/name.ML
changeset 33930 6a973bd43949
parent 33547 edfc35dcfe31
child 34307 9074aa7d06e0