src/Pure/General/name_space.ML
changeset 51085 d90218288d51
parent 50301 56b4c9afd7be
child 51510 b4f7e6734acc