remove_rules_for_term
Parse.remove_rules_for_term : string -> unit
Removes parsing/pretty-printing rules from the global grammar.
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.