src/Pure/context.ML
changeset 36619 deadcd0ec431
parent 36610 bafd82950e24
child 37216 3165bc303f66