src/Pure/variable.ML
changeset 70753 c5232e6fb10b
parent 70733 ce1afe0f3071
child 70843 cc987440d776