src/Pure/General/name_space.ML
changeset 41648 6d736d983d5c
parent 41254 78c3e472bb35
child 42135 da200fa2768c