clarified implicit Pure.thy;

careful export of type-dependent functions, without losing their special status;

observe ML print depth;

clarified Pretty.T toplevel pp;

clarified modules;

--HG--
rename : src/Pure/ML/install_pp_polyml.ML => src/Pure/ML/ml_pp.ML