src/Pure/General/name_space.ML
changeset 81304 228f4b9d1d67
parent 80298 f3bfec3b02f0
child 81531 b224e42b66f5