src/Pure/General/name_space.ML
changeset 74177 a8b032dede5c
parent 72053 4ed33ea8d957
child 74183 af81e4a307be