--- a/src/Tools/Code/code_target.ML Thu Jun 24 14:19:08 2010 +0200
+++ b/src/Tools/Code/code_target.ML Thu Jun 24 14:31:01 2010 +0200
@@ -142,9 +142,9 @@
name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
if serial1 = serial2 orelse not strict then
make_target ((serial1, serializer),
- ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),
+ ((merge (op =) (reserved1, reserved2), Symtab.merge (K true) (includes1, includes2)),
(merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
- Symtab.join (K snd) (module_alias1, module_alias2))
+ Symtab.join (K fst) (module_alias1, module_alias2))
))
else
error ("Incompatible serializers: " ^ quote target);