2010-06-01 ago merged
2010-06-01 ago assign now applies meet before update_new to avoid misleading error message.
2010-05-27 ago renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-02-06 ago fixed spelling;
2009-07-23 ago paramify_vars: Term_Subst.map_atypsT_same
2009-07-23 ago Purely functional type inference.
2009-07-17 ago tuned;
2009-07-14 ago tuned paramify_vars: Term_Subst.map_atypsT_option;
2009-07-09 ago renamed structure TermSubst to Term_Subst;
2009-02-27 ago eliminated NJ's List.nth;
2009-01-21 ago removed Ids;
2008-06-18 ago improved error output -- variant/mark bounds;
2007-10-04 ago replaced literal 'a by Name.aT;
2007-09-29 ago added fixate_params;
2007-09-23 ago constrain: canonical argument order;
2007-08-31 ago exported is_param;
2007-08-30 ago infer_types: general check_typs instead of Type.cert_typ_mode;
2007-08-14 ago infer_types: depend on Type.mode;
2007-04-23 ago added paramify_vars;
2007-04-15 ago moved get_sort to sign.ML;
2007-04-14 ago tuned comment;
2007-04-14 ago Term.string_of_vname;
2006-10-04 ago insert replacing ins ins_int ins_string
2006-09-27 ago internal params: Vartab instead of AList;
2006-09-21 ago tuned;
2006-07-19 ago Name.context for used'';
2006-07-11 ago Name.invent_list;
2006-05-05 ago added syntax for _type_constraint_;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-25 ago refer to structure Type instead of Sorts;
2006-02-15 ago removed distinct, renamed gen_distinct to distinct;
2006-02-11 ago tuned;
2006-02-10 ago decode: observe Syntax.constN;
2006-02-07 ago renamed gen_duplicates to duplicates;
2006-02-06 ago tuned;
2005-12-02 ago added mixfixT;
2005-09-20 ago slight adaptions to library changes
2005-09-06 ago AList.defined;
2005-09-06 ago introduced some new-style AList operations
2005-07-01 ago avoid polyeq;
2005-06-11 ago accomodate changed #classes;
2005-06-02 ago tuned;
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-06-22 ago tuned certify_typ/term;
2004-06-21 ago Type.cert_typ;
2004-06-01 ago removed obsolete sort 'logic';
2004-05-29 ago improved output; refer to Pretty.pp;
2004-05-21 ago incorporate type inference interface from type.ML;
2004-05-01 ago improved Term.invent_names;
2002-10-21 ago Replaced variantlist (quadratic) by gen_names (linear).
2002-10-07 ago take/drop -> splitAt
2000-03-30 ago support polymorphic Vars;
2000-01-05 ago support for dummy variables (anyT, logicT);
1999-09-29 ago handle Sorts.DOMAIN;
1998-10-09 ago Unified treatment of type error msgs.
1998-10-09 ago More pretty breaks in error msgs.
1998-05-25 ago remove seq2, scan (use seq2, foldl_map from library.ML);
1997-10-06 ago eliminated raise_term, raise_typ;
1997-07-09 ago improved type checking errors;