src/Pure/envir.ML
changeset 25517 36d710d1dbce
parent 25471 ca009b7ce693
child 26328 b2d6f520172c