140 Target { serial = serial2, serializer = _, |
140 Target { serial = serial2, serializer = _, |
141 reserved = reserved2, includes = includes2, |
141 reserved = reserved2, includes = includes2, |
142 name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) = |
142 name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) = |
143 if serial1 = serial2 orelse not strict then |
143 if serial1 = serial2 orelse not strict then |
144 make_target ((serial1, serializer), |
144 make_target ((serial1, serializer), |
145 ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)), |
145 ((merge (op =) (reserved1, reserved2), Symtab.merge (K true) (includes1, includes2)), |
146 (merge_name_syntax_table (name_syntax_table1, name_syntax_table2), |
146 (merge_name_syntax_table (name_syntax_table1, name_syntax_table2), |
147 Symtab.join (K snd) (module_alias1, module_alias2)) |
147 Symtab.join (K fst) (module_alias1, module_alias2)) |
148 )) |
148 )) |
149 else |
149 else |
150 error ("Incompatible serializers: " ^ quote target); |
150 error ("Incompatible serializers: " ^ quote target); |
151 |
151 |
152 fun the_serializer (Target { serializer, ... }) = serializer; |
152 fun the_serializer (Target { serializer, ... }) = serializer; |