Allow "_(" term ")" in the input syntax to request type inference

The goal is to allow pretty-printing such subexpressions as simple
underscores (or maybe as nothing, who knows?) for extra readability in LaTeX
output.

However, don't change `parens`, since it is used in too many places. Changing
`parens` would additionally allow things like:

f _(a b : type) ...

instead of

f (a b : type) ...

so add the _( ) syntax only to a variant of `parens` (which reuses the old code).