src/Pure/General/name_space.ML
changeset 62337 d3996d5873dd
parent 62241 a4a1f282bcd5
child 62967 5e8b1aead28f