src/Pure/General/name_space.ML
changeset 11307 891fbd3f4881
parent 9120 04a46ceace35
child 11829 f252646080fc