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);

removed pretty_theory, pprint_theory (see context.ML or thy_info.ML);
removed obsolete pretty_name_space;
accomodate identification of type Sign.sg and theory;

added type theory: generic theory contexts with unique identity,
arbitrarily typed data, linear and graph development -- a complete
rewrite of code that used to be spread over in sign.ML, theory.ML,
theory_data.ML, pure_thy.ML;

removed Pure/theory_data.ML;

added Id;

Theory.merge;

accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;
Context.theory_name;