75 consts: string Symtab.table, (*consts within the local scope*) |
75 consts: string Symtab.table, (*consts within the local scope*) |
76 fixes: (string * string) list, (*term fixes -- extern/intern*) |
76 fixes: (string * string) list, (*term fixes -- extern/intern*) |
77 binds: (typ * term) Vartab.table, (*term bindings*) |
77 binds: (typ * term) Vartab.table, (*term bindings*) |
78 type_occs: string list Symtab.table, (*type variables -- possibly within term variables*) |
78 type_occs: string list Symtab.table, (*type variables -- possibly within term variables*) |
79 maxidx: int, (*maximum var index*) |
79 maxidx: int, (*maximum var index*) |
80 sorts: sort OrdList.T, (*declared sort occurrences*) |
80 sorts: sort Ord_List.T, (*declared sort occurrences*) |
81 constraints: |
81 constraints: |
82 typ Vartab.table * (*type constraints*) |
82 typ Vartab.table * (*type constraints*) |
83 sort Vartab.table}; (*default sorts*) |
83 sort Vartab.table}; (*default sorts*) |
84 |
84 |
85 fun make_data (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) = |
85 fun make_data (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) = |