1\DOC remove_rules_for_term
2
3\TYPE {Parse.remove_rules_for_term : string -> unit}
4
5\SYNOPSIS
6Removes parsing/pretty-printing rules from the global grammar.
7
8\KEYWORDS
9Parsing, pretty-printing
10
11\LIBRARY
12Parse
13
14\DESCRIBE
15Calling {remove_rules_for_term s} removes all those rules (if any) in
16the global grammar that are for the term {s}.  The string specifies
17the name of the term that the rule is for, not a token that may happen
18to be used in concrete syntax for the term.
19
20\FAILURE
21Never fails.
22
23\EXAMPLE
24The universal quantifier can have its special binder status removed using
25this function:
26{
27   - val t = Term`!x. P x /\ ~Q x`;
28   <<HOL message: inventing new type variable names: 'a.>>
29   > val t = `!x. P x /\ ~Q x` : term
30   - remove_rules_for_term "!";
31   > val it = () : unit
32   - t;
33   > val it = `! (\x. P x /\ ~Q x)` : term
34}
35Similarly, one can remove the two rules for conditional
36expressions and see the raw syntax as follows:
37{
38   - val t = Term`if p then q else r`;
39   <<HOL message: inventing new type variable names: 'a.>>
40   > val t = `if p then q else r` : term
41   - remove_rules_for_term "COND";
42   > val it = () : unit
43   - t;
44   > val it = `COND p q r` : term
45}
46
47
48\COMMENTS
49There is a companion {temp_remove_rules_for_term} function,
50which has the same effect on the global grammar, but which does not
51cause this effect to persist when the current theory is exported.
52
53
54
55\SEEALSO
56Parse.remove_termtok.
57\ENDDOC
58