tuned fold on terms and lists;

tuned assoc;

tuned fold on terms; tuned assoc;

tuned min_key, max_key;

replaced foldl_XXX by canonical fold_XXX; canonical arguments for add_term_varnames, add_tvarsT, add_tvars, add_vars, add_frees,

tuned;

tuned fold on terms;

* Pure/library.ML: several combinators for linear functional transformations; * Pure/library.ML: canonical list combinators fold, fold_rev, and fold_yield; * Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types, fold_types;

optimize no_types_needed, remove exception handler

tuned;

lucas - slightly cleaned up. Removed redudent copy of Symtab structure.

* Improved 'oracle' command -- type-safe;

no open Logic;

removed itlist, rev_itlist -- use fold_rev, fold instead; improved end_itlist;

replaced itlist by fold_rev; replaced rev_itlist by fold;

replaced itlist by fold_rev;

use sys_error instead of exception Internal; actually use Termtab; tuned;

sys_error;

type-safe 'oracle' command;

added dest_table;

invoke_oracle: do not keep theory value, but theory_ref;

occs no longer infix (structure not open);

NameSpace.dest_table avoids duplicated extern;

with_path;