src/Pure/ML-Systems/use_context.ML
2009-03-23 wenzelm 2009-03-23 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;