src/Pure/General/name_space.ML
changeset 25456 6f79698f294d
parent 25225 e638164593bf
child 26440 feeb83f9657f