ML_Context.evaluate: proper context (for ML environment); use_text/use_file now depend on explicit ML name space;

ML_Context.evaluate: proper context (for ML environment);

simplified ML_Context.eval_in -- expect immutable Proof.context value;

proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);

simplified ML_Context.eval_in -- expect immutable Proof.context value; parse_code: operate on thy, which contains the ML environment;

explicit handling of ML environment within generic context; eval_wrapper: non-critical, struct_name is always Isabelle, tuned comments; eval_in/evaluate expect immutable Proof.context value; use_text/use_file now depend on explicit ML name space;

added ML_prf;

use_text/use_file now depend on explicit ML name space;

ML name space -- dummy version of Poly/ML 5.2 facility.

added ML-Systems/ml_name_space.ML;

use ML_prf within proofs;

local @{context};

moved global ML bindings to global place;

back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;

updated generated file;

wf_finite_psubset[simp], in_finite_psubset[simp]