src/Pure/context.ML
changeset 38820 d0f98bd81a85
parent 37871 c7ce7685e087
child 39020 ac0f24f850c9