----------------------------------------------------------------------
prefer_form_with_tok                                           (Parse)
----------------------------------------------------------------------
prefer_form_with_tok : {term_name : string, tok : string} -> unit

SYNOPSIS
Sets a grammar rule’s preferred flag, causing it to be preferentially printed.

KEYWORDS
Pretty-printing

LIBRARY
Parse

DESCRIBE
A call to {prefer_form_with_tok} causes the parsing/pretty-printing
rule specified by the {term_name}-{tok} combination to be the
preferred rule for pretty-printing purposes.  This change affects
the global grammar.

FAILURE
Never fails.

EXAMPLE
Imagine that one wants to use an infix {"U"} to stand for the {"UNION"} term.
This could be done as follows:

   > set_mapped_fixity {term_name = "UNION", fixity = Infixl 500,
                        tok = "U"};
   val it = () : unit

   > ``s U t``;
   val it = ``s U t`` : term

   > dest_term it;
   val it = COMB(``$UNION s``, ``t``) : lambda

Having made this change, one might prefer to see the form with {UNION}
printed:

   > prefer_form_with_tok {term_name = "UNION", tok = "UNION"};
   val it = () : unit

   > ``s U t``;
   val it = ``s UNION t`` : term


COMMENTS
As the example above demonstrates, using this function does not affect the
parser at all.

There is a companion {temp_prefer_form_with_tok} function, which has
the same effect on the global grammar, but which does not cause this
effect to persist when the current theory is exported.



----------------------------------------------------------------------