src/Pure/General/name_space.ML
changeset 8413 09db77a084aa
parent 6845 598d2f32d452
child 8728 33a9643ba626