added fixedN, constN;

tuned comment; moved local syntax to local_syntax.ML; common naming (for abbrevs and thms); transfer: merge consts; tuned pretty_term'; added polymorphic -- special case of generalize; added add_abbrevs(_i); read/cert: expand_consts;

tuned comment;

syntax: Context.generic;

Context.generic is canonical state of parsers; removed obsolete global/local parsers; tuned interfaces;

Local syntax depending on theory syntax.

decode: observe Syntax.constN;