src/Pure/context.ML
changeset 81656 7593c0976dc6
parent 80809 4a64fc4d1cde
child 83014 fa6c4ad21a24