2005-08-01 wenzelm [Mon, 01 Aug 2005 19:20:44 +0200] rev 16990
removed atless (use term_ord instead);
removed (inefficient) insert_aterm;
improved bound: nameless, avoid allocating new strings;
tuned sort_ord/typ_ord: dict_ord;
tuned abstract_over: SAME;
tuned add_term_vars/frees: OrdList.insert;
removed compress_type/compress_type (cf. compress.ML);
src/Pure/term.ML

2005-08-01 wenzelm [Mon, 01 Aug 2005 19:20:43 +0200] rev 16989
export MataSimplifier.inherit_bounds;
src/Pure/simplifier.ML

2005-08-01 wenzelm [Mon, 01 Aug 2005 19:20:42 +0200] rev 16988
Compress.typ;
src/Pure/sign.ML

2005-08-01 wenzelm [Mon, 01 Aug 2005 19:20:41 +0200] rev 16987
Compress.init_data;
src/Pure/pure_thy.ML

2005-08-01 wenzelm [Mon, 01 Aug 2005 19:20:40 +0200] rev 16986
nameless Term.bound;
src/Pure/net.ML src/Pure/pattern.ML

2005-08-01 wenzelm [Mon, 01 Aug 2005 19:20:39 +0200] rev 16985
improved bounds: nameless Term.bound, recover names for output;
src/Pure/meta_simplifier.ML

2005-08-01 wenzelm [Mon, 01 Aug 2005 19:20:38 +0200] rev 16984
tuned dict_ord;
src/Pure/library.ML

2005-08-01 wenzelm [Mon, 01 Aug 2005 19:20:37 +0200] rev 16983
replaced atless by term_ord;
src/Pure/Proof/extraction.ML src/Pure/Proof/reconstruct.ML src/Pure/drule.ML src/Pure/proofterm.ML

2005-08-01 wenzelm [Mon, 01 Aug 2005 19:20:36 +0200] rev 16982
chain_history: turned into runtime flag;
added monomorphic;
removed (inefficient) fast_overloading_info;
Compress.typ;
tuned;
src/Pure/defs.ML

2005-08-01 wenzelm [Mon, 01 Aug 2005 19:20:35 +0200] rev 16981
compression of terms and types by sharing common subtrees;
src/Pure/compress.ML