src/Pure/name.ML
changeset 20189 1be8b181dafa
parent 20174 c057b3618963
child 20192 956cd30ef3be