src/Pure/ML/ml_env.ML
2010-04-16 wenzelm 2010-04-16 proper masking of dummy name_space;
2010-04-16 wenzelm 2010-04-16 proper checking of ML functors (in Poly/ML 5.2 or later); eliminated pathetic comments;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-06-06 wenzelm 2009-06-06 tuned comments;
2009-06-04 wenzelm 2009-06-04 eliminated costly registration of tokens;
2009-06-01 wenzelm 2009-06-01 tuned signature;
2009-06-01 wenzelm 2009-06-01 maintain tokens within common ML environment;
2009-06-01 wenzelm 2009-06-01 moved local ML environment to separate module ML_Env;