src/Pure/General/symbol.scala
changeset 57978 8f4a332500e4
parent 57840 074cb68b40a8
child 59107 48429ad6d0c8