1structure type_grammar_dtype =
2struct
3
4datatype grammar_rule =
5         INFIX of {opname : string, parse_string : string} list *
6                  HOLgrammars.associativity
7
8datatype type_structure =
9         TYOP of {Thy : string, Tyop : string, Args : type_structure list}
10       | PARAM of int
11
12datatype delta =
13         NEW_TYPE of KernelSig.kernelname
14       | NEW_INFIX of {Name : string, ParseName : string,
15                       Assoc : HOLgrammars.associativity, Prec : int}
16       | TYABBREV of KernelSig.kernelname * Type.hol_type * bool
17       | DISABLE_TYPRINT of string
18       | RM_KNM_TYABBREV of KernelSig.kernelname
19       | RM_TYABBREV of string
20
21end
22