src/Pure/context.ML
changeset 21315 be2669fe8363
parent 20926 b2f67b947200
child 21518 571b8cd087f8