gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
#hard-wired components
src/Tools/Code
src/Tools/jEdit
src/Tools/Graphview
src/HOL/Mirabelle
src/HOL/Mutabelle
src/HOL/Library/Sum_of_Squares
src/HOL/Tools
src/HOL/Tools/ATP
src/HOL/TPTP