- CURRY_CONV (Term `(\(x,y). x + y) (1,2)`);
> val it = |- (\(x,y). x + y) (1,2) = (\x y. x + y) 1 2 : thm
- CURRY_CONV (Term `(\(x,y). x + y) z`);
> val it = |- (\(x,y). x + y) z = (\x y. x + y) (FST z) (SND z) : thm
FAILURE
CURRY_CONV tm fails if tm is not an application of a paired abstraction.