src/Pure/context.ML
changeset 38173 de6ef87e65b3
parent 37871 c7ce7685e087
child 39020 ac0f24f850c9