There is a pretty-printer installed in the interactive system so that
term grammar values are presented nicely. The global term grammar is
passed as a parameter to the Term parsing function in the Parse
structure, and also drives the installed term and theorem
pretty-printers.