src/Pure/variable.ML
changeset 62597 b3f2b8c906a6
parent 62012 12d3edd62932
child 62771 dd2914250ca7