2005-06-05 ago added Type.freeze(_type);
2005-04-21 ago - Eliminated nodup_vars check.
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-06-22 ago tuned;
2004-06-22 ago tuned certify_typ/term;
2004-06-21 ago tuned certify_typ;
2004-06-09 ago tuned messages;
2004-05-29 ago removed norm_typ; improved output; refer to Pretty.pp;
2004-05-21 ago major cleanup of tsig datastructures and extend/merge operations; fixes old bugs in classes/arities code; proper treatment of nonterminals and syntax-only types;
2002-10-21 ago Removed add_env because was too slow for large environments.
2002-01-12 ago paramify_dummies: proper treatment of maxidx;
2001-12-18 ago tuned interface of unify, param;
2001-12-14 ago varify returns newly introduced variables;
2001-11-28 ago Syntax.typ_of_term: pass intern sort fn;
2001-11-16 ago ext_tsig_classes: rebuild_tsig!!!!!
2001-02-01 ago ext_classrel: certify_class;
2000-11-18 ago export freeze_thaw_type;
2000-08-03 ago typ_no_norm;
2000-05-21 ago removed is_type_abbr;
2000-04-17 ago NameSpace.is_qualified;
2000-04-14 ago added is_type_abbr;
2000-03-30 ago tuned;
2000-03-10 ago Type.unify and Type.typ_match now use Vartab instead of association lists.
1999-09-29 ago added witness_sorts, univ_witness;
1999-08-18 ago freeze_thaw does nothing if no variables
1999-07-23 ago replaced assoc lists by Symtab.table;
1998-08-19 ago fixed param;
1998-06-25 ago defaults for free variables hide consts of same name;
1998-05-28 ago fixed error msgs;
1998-02-05 ago added param;
1997-11-05 ago fixed exception OPTION;
1997-10-10 ago decode: qualified is always const;
1997-10-07 ago tuned decode;
1997-10-06 ago eliminated raise_term, raise_typ;
1997-06-05 ago Removal of freeze_vars and thaw_vars. New freeze_thaw
1997-05-13 ago of_sort: type_sig -> typ * sort -> bool;
1997-04-18 ago tuned check_has_sort;
1997-04-17 ago improved type check error messages;
1997-04-16 ago moved classes / sorts to sorts.ML;
1997-03-07 ago Removed some polymorphic equality tests
1997-02-21 ago Replaced "flat" by the Basis Library function List.concat
1997-02-14 ago Added optimization: do nothing for empty list
1997-02-10 ago fixed comment;
1997-02-06 ago added eq_sort (will move to sorts.ML eventually);
1996-11-28 ago Tidying and renaming of function Dom
1996-11-26 ago Removed or eta-expanded some declarations that are illegal under value
1996-11-13 ago Removal of polymorphic equality via mem, subset, eq_set, etc
1996-11-01 ago maxidx_of_typs replaces max o map maxidx_of_typ
1996-03-28 ago Optimized type inference (avoids chains of
1996-02-16 ago Elimination of fully-functorial style.
1996-02-09 ago renamed expand_typ to norm_typ
1996-01-29 ago inserted tabs again
1996-01-29 ago removed tabs
1996-01-11 ago Removed bug in type unification. Negative indexes are not used any longer.
1995-12-08 ago infer_types now takes a term list and a type list as argument. It
1995-09-21 ago added comment;
1995-09-01 ago nonempty_sort: no longer var names as args;
1995-08-01 ago added nonempty_sort (a somewhat braindead version!);