src/Pure/General/name_space.ML
changeset 50073 7e8994098347
parent 49816 e63d6c55ad6d
child 50201 c26369c9eda6