Remove unused (obsolete) Muon tools

As mentioned in this comment, there are unused Muon tools -- at least, they will be unused as soon as !3484 (merged) is merged. This MR removes them. So this should be merged shortly after !3484 (merged) is merged.