I currently supervise a student who's investigating proof refactoring. One
possible outcome of this would be a tool that also does what you suggested.
It's a little too early to tell, though.
On 8 July 2017 23:28:42 CEST, Lawrence Paulson wrote:
A while ago, Florian Haftmann sent a command that does something like this to
the mailing list . I attach a version that works with current Isabelle2016-1
(not sure if I got all the modifications right, but it seems to work at least
on the example in the .thy file).