Allow pattern-overloading to work with paired abstractions

[mn200]

When parsing, the system doesn't do a paired β-reduction, and when printing, it doesn't recognise the term as an abstraction, and so fails to do any useful pattern-matching.

[mn200]

For example, it would be nice to be able to do

overload_on("Foo", ``λ(x,y). x + y * 2``)

and then have occurrences of the pattern get printed as, e.g.,

Foo(3,z+1)

If one typed Foo p, then the printer would probably come back with

(λ(x,y). Foo(x,y)) p

but I don’t think that’s a big problem.

[acjf3]

This seems to have been implemented.

[mn200]

This session shows that things are still not quite right:

> overload_on("Foo", ``λ(x,y). x + y * 2``);
val it = (): unit
> ``2 + 3 * 2``;
val it = ``2 + 3 * 2``: term
> ``Foo(2,3)``;
val it = ``Foo (2,3)``: term
> dest_term it;
val it = COMB (``λ(x,y). x + y * 2``, ``(2,3)``): lambda