src/Pure/General/name_space.ML
changeset 28154 3c3663e24ba7
parent 27196 ef2f01da7a12
child 28860 b1d46059d502