src/Pure/name.ML
changeset 28822 7ca11ecbc4fb
parent 28821 78a6ed46ad04
child 28860 b1d46059d502