# HG changeset patch
# User wenzelm
# Date 1277382661 -7200
# Node ID 42804fb5dd921338f7b2ad4d452c47f62fd1f818
# Parent  d9c2fdd6614f3d99bda0c46b412542559e2c4875
slightly more standard data merge: Symtax.merge (K true) avoids equality on abstract type Pretty.T and gracefully accepts overriding, Symtab.join prefers first entry as usual;

diff -r d9c2fdd6614f -r 42804fb5dd92 src/Tools/Code/code_target.ML
--- 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);