src/Pure/context.ML
changeset 11545 0b56d9c90dcf
parent 10924 92305ae9f460
child 11819 9283b3c11234