src/Pure/name_space.ML
changeset 4550 53553ccda0e6
parent 4497 2ba0730672c9
child 4851 cbbc53963aaa