src/Pure/General/name_space.ML
changeset 27094 2cf13a72e170
parent 26657 35249f5367b3
child 27196 ef2f01da7a12