102 fun make_data |
102 fun make_data |
103 (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) = |
103 (is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints) = |
104 Data {is_body = is_body, names = names, consts = consts, bounds = bounds, fixes = fixes, |
104 Data {is_body = is_body, names = names, consts = consts, bounds = bounds, fixes = fixes, |
105 binds = binds, type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints}; |
105 binds = binds, type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints}; |
106 |
106 |
|
107 val empty_data = |
|
108 make_data (false, Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty, |
|
109 Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty)); |
|
110 |
107 structure Data = Proof_Data |
111 structure Data = Proof_Data |
108 ( |
112 ( |
109 type T = data; |
113 type T = data; |
110 fun init _ = |
114 fun init _ = empty_data; |
111 make_data (false, Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty, |
|
112 Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty)); |
|
113 ); |
115 ); |
114 |
116 |
115 fun map_data f = |
117 fun map_data f = |
116 Data.map (fn |
118 Data.map (fn |
117 Data {is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints} => |
119 Data {is_body, names, consts, bounds, fixes, binds, type_occs, maxidx, sorts, constraints} => |