src/Pure/context.ML
changeset 24834 5684cbf8c895
parent 24559 dae0972c0066
child 26413 003dd6155870