src/Pure/context.ML
changeset 8720 840c75ab2a7f
parent 8348 ebbbfdb35c84
child 8801 9d01c9a26134