src/Pure/context.ML
changeset 30227 853abb4853cc
parent 29368 503ce3f8f092
child 30628 4078276bcace