src/Pure/General/name_space.ML
changeset 37813 7c33f5c5c59c
parent 35679 da87ffdcf7ea
child 41254 78c3e472bb35