mk_pair : term * term -> term
STRUCTURE
SYNOPSIS
Constructs object-level pair from a pair of terms.
DESCRIPTION
mk_pair (t1,t2) returns (t1,t2).
FAILURE
Never fails.
SEEALSO
HOL  Trindemossen-1