src/Pure/General/name_space.ML
changeset 40650 d40b347d5b0b
parent 35679 da87ffdcf7ea
child 41254 78c3e472bb35