src/Pure/context.ML
changeset 8657 b9475dad85ed
parent 8348 ebbbfdb35c84
child 8801 9d01c9a26134