src/Pure/General/name_space.ML
changeset 23613 3f2a6c66e089
parent 23086 12320f6e2523
child 23668 8b5a2a79a6e3
equal deleted inserted replaced
23612:52c7bcfc9515 23613:3f2a6c66e089