added pretty_sg; added infer_types; removed subclasses arg of add_classes; removed old 'extend' and related stuff; various minor internal changes;

added add_defs, add_defs_i;

cleaned sig; removed add_defns (now in drule.ML as add_defs); removed add_sigclass; minor internal changes;

added theory_of_sign, theory_of_thm; renamed get_thms to thms_of; improved store_thms etc.;

renamed 'defns' to 'defs'; removed 'sigclass'; replaced parents by enclose; exported parens, brackets, mk_list, mk_big_list, mk_pair, mk_triple; various minor internal changes;

added raw_term_sorts and changed typ_of_term accordingly (part of fix of the typevar-sort-constraint BUG); various minor internal changes;

added type xrule (from sextension.ML); removed old 'extend'; removed added syn_ext_const_names, syn_ext_trfuns (now in syn_ext.ML); various minor changes;

removed idT, varT, tidT, tvarT (now in lexicon.ML); added syn_ext_const_names, syn_ext_trfuns;

various minor internal changes;

added map_strs: (string -> string) -> T -> T;

removed roots arg of extend_gram; added functor sig constraint (: PARSER);

minor cleanings;

replaced id, var, tid, tvar by idT, varT, tidT, tvarT; added const, free, var: build atomic terms of dummyT; added 'xnum' (signed numerals) and 'xstr' (strings) token kinds; various minor internal changes;

replaced SExtension by SynTrans (mixfix stuff in Mixfix); private structs now hidden within PrivateSyntax;