src/Pure/name_space.ML
changeset 4003 2bbeed529077
parent 3993 f88e0f0e2666
child 4101 e8ad51c88be9