Def uncurry == f:'a'b'c. p:'a'b. f(1of(p),2of(p))

is mentioned by

Thm* 'c,'a,'b:S. Thm* all Thm* (f:'a  'b  'c. all Thm* (f:'a  'b  'c. (x:'a. all Thm* (f:'a  'b  'c. (x:'a. (y:'b. equal(uncurry(f,pair(x,y)),f(x,y)))))

[huncurry_def]

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html