src/Pure/context.ML
changeset 9172 2dbb80d4fdb7
parent 8801 9d01c9a26134
child 9586 f6669dead969