src/Pure/context.ML
changeset 21125 9b7d35ca1eef
parent 20926 b2f67b947200
child 21518 571b8cd087f8