Regression: X = f\f (X (y\e))

[robblanco]

From test/test_unify.ml (and unrelated to the changes in #58):

Failure: Abella:0:Unify:50:X = f\f (X (y\e))

OUnit: expected: x1\x1 (X (x2\e)) but got: x1\x1 (X x2\e)

It looks like a simple formatting issue.

[chaudhuri]

Yes, this is a result of the new pretty printer for terms and metaterms that tries to produce parentheses in a more "human-like" fashion. Since \ has higher precedence than function application---which is why expressions such as pi x\ f x parse---there is no need to parenthesize here.

We'll close this after updating the test.