src/Pure/ML-Systems/polyml_old_compiler4.ML
2009-01-19 wenzelm 2009-01-19 removed Ids;
2008-09-17 wenzelm 2008-09-17 use_text/use_file now depend on explicit ML name space;
2008-05-14 wenzelm 2008-05-14 use_file: pass str_of_pos;
2008-05-14 wenzelm 2008-05-14 use_text/file: ignore str_of_pos argument;
2008-03-31 wenzelm 2008-03-31 before close: Exn.capture/release;
2008-03-24 wenzelm 2008-03-24 ML runtime compilation: pass position, tuned signature;
2008-03-24 wenzelm 2008-03-24 Runtime compilation -- for old version of PolyML.compiler (version 4.x).