src/Pure/context.ML
changeset 23597 ab67175ca8a5
parent 23595 7ca68a2c8575
child 23944 2ea068548a83