src/Pure/General/name_space.ML
changeset 41171 043f8dc3b51f
parent 35679 da87ffdcf7ea
child 41254 78c3e472bb35