src/Pure/name_space.ML
changeset 4098 71e05eb27fb6
parent 3993 f88e0f0e2666
child 4101 e8ad51c88be9