src/Pure/variable.ML
changeset 70823 c6f2a73987cd
parent 70733 ce1afe0f3071
child 70843 cc987440d776