clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
apply_end cases are no longer seen in current context section (hardly relevant in practice);
#hard-wired components
src/Tools/jEdit
src/Tools/Graphview
src/HOL/Mirabelle
src/HOL/Mutabelle
src/HOL/Library/Sum_of_Squares
src/HOL/SPARK
src/HOL/Tools
src/HOL/Tools/ATP
src/HOL/TPTP