eliminated ASCII syntax from Pure bootstrap;
tuned comments;

tuned messages -- more symbols;

PIDE reports of implicit variable scope;

more rigid check of lhs;

within a proof body context, undeclared frees are like global constants;
tuned signature;

more qualified names;

renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;

tuned;

modernized signature of Term.absfree/absdummy;
eliminated obsolete Term.list_abs_free;

explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;

--HG--
rename : src/Pure/Syntax/syn_trans.ML => src/Pure/Syntax/syntax_trans.ML

moved Primitive_Defs.mk_defpair to OldGoals.mk_defpair;

modernized structure Primitive_Defs;

moved basic algebra of long names from structure NameSpace to Long_Name;

renamed NameSpace.base to NameSpace.base_name;
renamed NameSpace.map_base to NameSpace.map_base_name;
eliminated alias Sign.base_name = NameSpace.base_name;

dropped ID

dest/cert_def: replaced Pretty.pp by explicit Proof.context;

Primitive definition forms.