src/Pure/General/name_space.ML
changeset 36947 285b39022372
parent 35679 da87ffdcf7ea
child 41254 78c3e472bb35