src/Pure/General/name_space.ML
changeset 55841 a232c0ff3c20
parent 55840 2982d233d798
child 55845 a05413276a0d