equal
deleted
inserted
replaced
184 |
184 |
185 structure Targets = Theory_Data |
185 structure Targets = Theory_Data |
186 ( |
186 ( |
187 type T = (target * Code_Printer.data) Symtab.table * int; |
187 type T = (target * Code_Printer.data) Symtab.table * int; |
188 val empty = (Symtab.empty, 0); |
188 val empty = (Symtab.empty, 0); |
189 val extend = I; |
|
190 fun merge ((targets1, index1), (targets2, index2)) : T = |
189 fun merge ((targets1, index1), (targets2, index2)) : T = |
191 let |
190 let |
192 val targets' = |
191 val targets' = |
193 Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) => |
192 Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) => |
194 if #serial target1 = #serial target2 then |
193 if #serial target1 = #serial target2 then |