* Pure: structure OrdList (cf. Pure/General/ord_list.ML); * Pure: more efficient orders for basic syntactic entities;

added ST combinator '|->'

Symtab: use fast_string_ord instead of string_ord -- affects order of Symtab.dest etc.;

tuned;

made smlnj happy;

methods: added simp_flags argument, added "depth_limit" flag;

added transform_exceptions: bool ref;

tuned;

dummy exception_trace;

tuned union: avoid garbage in trivial case;

dest_ctyp: raise exception for non-constructor; dest_comb: replaced expensive fastype_of by Term.argument_type; dest_abs: replaced expensive variant_abs by Term.dest_abs; hyps: fast_term_ord;

added fast_indexname_ord, fast_term_ord; changed sort_ord, typ_ord, Vartab, Termtab: use fast orders; added argument_type_of, dest_abs; tuned;

use fast_string_ord;

added fast_string_ord;

Streamlined the signal handler in watcher.ML

unified main and dist

started unifying main and dist

(intermediate commit)

Simple report generator for Poly/ML profiling output.

tuned;

ambig msg: warning again;

avoid polyeq;

tuned term_ord: less garbage;

cterm_aconv: avoid rep_cterm;

decomp_simp: compare terms, not cterms;

back to 1.28;

prime is a predicate now.

* Isar profiling: new reference Toplevel.profiling (default 0);

use tracing for potentially voluminous ambiguity output;

added profiler interface (dummy);