src/Pure/General/name_space.ML
changeset 15900 d6156cb8dc2e
parent 15624 484178635bd8
child 16002 e0557c452138