removed unused info channel;

renamed Output.has_mode to print_mode_active;

tuned comment;

cleaned-up Output functions; removed unused info channel; moved print_mode to ROOT.ML (generic non-sense);

improved exception CTERM; added instantiate_cterm; removed obsolete sign_of_thm;

added scanwords from library.ML (for obsolete rename_tac);

removed obsolete scanwords (see obsolete tactic.ML:rename_tac for its only use);

removed dead code;

cleaned-up Output functions;

eliminated obsolete rename_tac;

removed obsolete sign_of/sign_of_thm;

ML antiquotes;

tuned comments;

fixed chr/explode;

avoid overloaded integer constants (accomodate Alice);

avoid clash with Alice keywords;

signature: eqtype to accomodate Alice;

renamed comp to compose (avoid clash with Alice keywords);

renamed of_sort_derivation record fields (avoid clash with Alice keywords);

added ML-Systems/alice.ML;

renamed Variable.import to import_thms (avoid clash with Alice keywords);

removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);

ranamed CodegenData.lazy to lazy_thms (avoid clash with Alice keywords);

remove the lemma swap_fun which was not needed

slighltly improved the proof of unicity

Compatibility file for Alice 1.3 -- experimental!

rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name

optimizing the null instantiation case

now exports distinct_subgoal_tac (needed by MetisAPI)

exception handling