let
term_mk_apply =
Apply
.mk_apply
Th
.sigma
None