added theorem_space; removed unused extern_thm_sg; accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; removed theory management (cf. 'history' in context.ML); moved add_typedecls to sign.ML; Sign.init, Theory.init; tuned;

Context.theory_name; tuned;

added serial numbers;

removed obsolete pretty printers for Theory.theory, Sign.sg; added pretty printer for Context.theory (long form of output);