Parse.remove_rules_for

STRUCTURE

SYNOPSIS

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

LIBRARY

Parse

DESCRIPTION

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

remove_termtok