src/Pure/envir.ML
changeset 435 ca5356bd315a
parent 247 bc10568855ee
child 719 e3e1d1a6d408