src/Pure/envir.ML
changeset 23024 70435ffe077d
parent 22678 23963361278c
child 24670 9aae962b1d56