src/Pure/name_space.ML
changeset 3864 e0ce3d4ec47d
parent 3833 370e845c391f
child 3876 e6f918979f2d