src/Pure/General/name_space.ML
changeset 10168 50be659d4222
parent 9120 04a46ceace35
child 11829 f252646080fc