I don't use clausal function definition, but still I think that you don't want to only warn on unused args if they are unused accross all cases. If you did that then one case which forgot to use one of its args would cause no message. Clearly it is all a matter of balance here, so I don't know which way is best.