pair_of_list : 'a list -> 'a * 'a
STRUCTURE
SYNOPSIS
Turns a two-element list into a pair.
DESCRIPTION
pair_of_list [x, y] returns (x, y).
FAILURE
Fails if applied to a list that is not of length 2.
SEEALSO
HOL  Trindemossen-1