src/Pure/context.ML
changeset 7701 2c8c3b7003e5
parent 6310 353a8a9d9d2c
child 8348 ebbbfdb35c84