Yes, function rules should be applied by pattern match rather than unification, except in test generation. I have added a comment and will revise it to include the case of test generation when I start to work on that.