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;
1997-04-18 ago tuned err msg;
1997-04-17 ago tuned error msgs;
1997-04-17 ago improved type check error messages;
1997-04-16 ago Type inference (isolated from type.ML, completely reimplemented).