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