src/Pure/General/name_space.ML
changeset 76378 c0566b6f6ca8
parent 75983 34dd96a06c45
child 77815 c3330a54b9e5