src/Pure/General/name_space.ML
changeset 58229 cece11f6262a
parent 57899 5867d1306712
child 58668 1891f17c6124