src/Pure/context.ML
changeset 78843 fc3ba0a1c82f
parent 78464 12af46f2cd94
child 79076 a1b5357b5473