src/Pure/context.ML
changeset 24077 e7ba448bc571
parent 23944 2ea068548a83
child 24141 73baca986087