Commented out with #if 0 so that we can easily undo this change if in the future it turns out that this introduces other problems.
Simply removed it in pattern_match_old as it is obsolete and should not be used anymore anyways.
(Note however that the problem example in issue #2398 (closed) is however caused by one such function making use of this outdated pattern matching utility.)
Closes #2398 (closed)