src/Pure/General/name_space.ML
changeset 27895 e4f8763b971b
parent 27196 ef2f01da7a12
child 28860 b1d46059d502