added command 'ML_export';

more symbols;

proper support for recursive ML debugging;

tuned signature;
proper signature for structure;

explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
handle bootstrap signatures as well;

more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
avoid slowdown of Resources.loaded_files due to command name 'use' in Pure base syntax;

clarified modules;
tuned signature;

clarified modules -- simplified bootstrap;

clarified bootstrap environment;

support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;

clarified SML name space: no access to structure PolyML;

explicit print_depth for the sake of Spec_Check.determine_type;

tuned signature;

tuned signature;

clarified modules;

--HG--
rename : src/Pure/RAW/compiler_polyml.ML => src/Pure/RAW/ml_compiler0.ML

load secure.ML earlier;
eliminated obsolete ml_parse.ML;
tuned signature;

--HG--
rename : src/Pure/General/secure.ML => src/Pure/RAW/secure.ML

SML/NJ is no longer supported;

evaluate ML expressions within debugger context;
redirected writeln/warning for ML compiler;

store breakpoints within ML environment;

more careful handling of auxiliary environment structure -- allow nested ML evaluation;

renamed "pairself" to "apply2", in accordance to @{apply 2};

added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;

added command 'SML_file' for Standard ML without Isabelle/ML add-ons;

clarified bootstrap process: switch to ML with context and antiquotations earlier;

renamed Position.str_of to Position.here;

proper masking of dummy name_space;

proper checking of ML functors (in Poly/ML 5.2 or later);
eliminated pathetic comments;

adapted Generic_Data, Proof_Data;
tuned;

tuned comments;

eliminated costly registration of tokens;

tuned signature;

maintain tokens within common ML environment;

moved local ML environment to separate module ML_Env;