src/Pure/General/name_space.ML
changeset 66787 64b47495676d
parent 66249 f50e6e31a0ee
child 68163 b168f30e541f