src/Pure/name.ML
changeset 33096 db3c18fd9708
parent 33095 bbd52d2f8696
child 33547 edfc35dcfe31