src/Pure/envir.ML
changeset 20522 05072ae0d435
parent 20098 19871ee094b1
child 20548 8ef25fe585a8