src/Pure/General/name_space.ML
changeset 45633 2cb7e34f6096
parent 45412 7797f5351ec4
child 45666 d83797ef0d2d