src/Pure/name.ML
changeset 29427 7ba952481e29
parent 29006 abe0f11cfa4e
child 30584 7e839627b9e7