removed old-style theory format; tuned;

avoid lagacy read function;

added thm(s) retrieval functions (from goals.ML);

removed obsolete old-locales; moved thm(s) retrieval functions back to pure_thy.ML; removed atomic_goal(w) interface; removed user-level (top_sg, prin, printyp, pprint_term/typ, which tend to cause some confusion about the implicit goal (!) context being used here;