src/Pure/context.ML
changeset 62842 db9f95ca2a8f
parent 62819 d3ff367a16a0
child 62876 507c90523113