----------------------------------------------------------------------
remove_rules_for_term                                          (Parse)
----------------------------------------------------------------------
Parse.remove_rules_for_term : string -> unit

SYNOPSIS
Removes parsing/pretty-printing rules from the global grammar.

KEYWORDS
Parsing, pretty-printing

LIBRARY
Parse

DESCRIBE
Calling {remove_rules_for_term s} removes all those rules (if any) in
the global grammar that are for the term {s}.  The string specifies
the name of the term that the rule is for, not a token that may happen
to be used in concrete syntax for the term.

FAILURE
Never fails.

EXAMPLE
The universal quantifier can have its special binder status removed using
this function:

   - val t = Term`!x. P x /\ ~Q x`;
   <<HOL message: inventing new type variable names: 'a.>>
   > val t = `!x. P x /\ ~Q x` : term
   - remove_rules_for_term "!";
   > val it = () : unit
   - t;
   > val it = `! (\x. P x /\ ~Q x)` : term

Similarly, one can remove the two rules for conditional
expressions and see the raw syntax as follows:

   - val t = Term`if p then q else r`;
   <<HOL message: inventing new type variable names: 'a.>>
   > val t = `if p then q else r` : term
   - remove_rules_for_term "COND";
   > val it = () : unit
   - t;
   > val it = `COND p q r` : term




COMMENTS
There is a companion {temp_remove_rules_for_term} 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.



SEEALSO
Parse.remove_termtok.

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