prefer_form_with_tok : {term_name : string, tok : string} -> unit
STRUCTURE
Parse
SYNOPSIS
Sets a grammar rule’s preferred flag, causing it to be preferentially printed.
LIBRARY
Parse
DESCRIPTION
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.

HOL  Kananaskis-13