src/Pure/variable.ML
changeset 69510 0f31dd2e540d
parent 67721 5348bea4accd
child 69575 f77cc54f6d47