src/Pure/name.ML
changeset 29031 e74341997a48
parent 29006 abe0f11cfa4e
child 30584 7e839627b9e7