2011-06-09 ago tuned signature: Name.invent and Name.invent_names;
2011-04-19 ago split Type_Infer into early and late part, after Proof_Context;
2011-04-19 ago more precise treatment of existing type inference parameters;
2011-04-18 ago tuned;
2011-04-18 ago simplified pretty printing context, which is only required for certain kernel operations;
2011-04-16 ago modernized structure Proof_Context;
2011-04-08 ago explicit structure Syntax_Trans;
2011-03-28 ago address serious problem of type inference (introduced in 6f085332c7d3): _type_constraint_ needs type scheme A --> A with proper scope of parameters, otherwise term "(f :: _ => _) :: 'c => 'c" will get type "'a => 'b", for example;
2010-10-29 ago more sharing of operations, without aliases;
2010-09-13 ago tuned signature;
2010-09-13 ago Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
2010-09-13 ago simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
2010-09-12 ago Type_Infer.preterm: eliminated separate Constraint;
2010-09-12 ago Type_Infer.infer_types: plain error instead of kernel exception TYPE;
2010-09-12 ago load type_infer.ML later -- proper context for Type_Infer.infer_types;
2010-09-12 ago common Type.appl_error, which also covers explicit constraints;
2010-09-12 ago eliminated aliases of Type.constraint;
2010-09-12 ago tuned;
2010-09-12 ago tuned messages;
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;