moved ProofContext.pretty_thm to Display.pretty_thm etc.;
explicit old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
removed some very old thm print operations;
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
load display.ML after assumption.ML, to accomodate proper contextual theorem display;