src/Pure/General/name_space.ML
changeset 16081 81a4b4a245b0
parent 16002 e0557c452138
child 16137 00e9ca1e7261