Pure: clear separation of logical types and nonterminals;

adapted tsig/sg interface;

added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;

added fold, product; removed transitive_closure;

adapted names of some sort ops;

major cleanup of tsig datastructures and extend/merge operations; fixes old bugs in classes/arities code; proper treatment of nonterminals and syntax-only types;

Type.strip_sorts;

incorporate type inference interface from type.ML;

adapted tsig interface;

moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);

test_classrel/arity improve error reporting; tuned;

xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;

string_of_vname moved to term.ML;

incorporate sort ops from term.ML; use Graph.T; misc cleanup;

type.ML now before Syntax module;

xxx_typ_raw replace xxx_typ_no_norm forms;

'classrel' now allows multiple arguments;

Sign.certify_tyname;

TypeInfer.paramify_dummies, TypeInfer.param;

Args.local_typ_raw;

output_tym: removed duplicate clauses;

Graph.minimals;

adapted syntax to cope with lack of non-logical types;

Type.typ_instance;

load ML files only once;

removed duplicate thms;

Sign.typ_instance;

tuned message;

tuned document;

use plain SOME;

proper use of 'syntax';

auto update