thy_deps: sort Context.thy_ord;

added thy_ord -- order of creation; ancestors: back to traditional ad-hoc order (avoid occasional problems with get_thm);

simplified thy_deps using Theory.ancestors_of (in order of creation);

renamed Variable.importT to importT_thms;

removed unused dep_graph;

theory: maintain ancestors in order of creation;

rep_thm/cterm/ctyp: removed obsolete sign field; renamed Variable.importT to importT_thms;

rebind HOL.refl as refl (hidden by widen.refl);

rep_thm/cterm/ctyp: removed obsolete sign field;

make fresh_guess fail if it does not solve the subgoal

add a few details in the Fst and Snd cases of unicity proof

find_first is just an alias

added print_mode (generic non-sense);

improved exception CTERM; removed obsolete sign_of/sign_of_thm;

removed unused info channel; renamed Output.has_mode to print_mode_active; cleaned-up Output functions;

added print_mode;

removed unused info channel;

renamed Output.has_mode to print_mode_active;

tuned comment;

cleaned-up Output functions; removed unused info channel; moved print_mode to ROOT.ML (generic non-sense);

improved exception CTERM; added instantiate_cterm; removed obsolete sign_of_thm;

added scanwords from library.ML (for obsolete rename_tac);

removed obsolete scanwords (see obsolete tactic.ML:rename_tac for its only use);

removed dead code;

cleaned-up Output functions;

eliminated obsolete rename_tac;

removed obsolete sign_of/sign_of_thm;

ML antiquotes;