removed use of CharVector in generated parser, to make SMLNJ happy

merged

normalize defs (again, cf. 008b7858f3c0);

some context examples;

retain literal non-HHF assumptions, to facilitate re-import in Generic_Target.import_export_proof;

another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix);

export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);

better drop background syntax if entity depends on parameters;
more direct Type_Infer_Context.const_type instead of Syntax.check_term, which expands abbreviations (and potentially more);

more uniform abbrev vs. define;

tuned;