src/Pure/name_space.ML
changeset 4552 bb8ff763c93d
parent 4497 2ba0730672c9
child 4851 cbbc53963aaa