src/Pure/variable.ML
changeset 21125 9b7d35ca1eef
parent 20797 c1f0bc7e7d80
child 21287 a713ae348e8a