src/Pure/General/name_space.ML
changeset 24878 7ed3077528b6
parent 24361 52a14669f9e9
child 25072 03f57b516e12