src/Pure/envir.ML
changeset 72051 438adb97d82c
parent 63619 9c870388e87a
child 74232 1091880266e5