# HG changeset patch
# User haftmann
# Date 1280135710 -7200
# Node ID f37a8d48810508bd6c8b14bc156a7f6535634e01
# Parent  278367fa09f3737c7ded35600e5718ccd72939d8
restored unusual snd-biased merge/join policy -- required due to non-conservative code setups

diff -r 278367fa09f3 -r f37a8d488105 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Mon Jul 26 11:11:10 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Mon Jul 26 11:15:10 2010 +0200
@@ -141,9 +141,9 @@
       name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
   if serial1 = serial2 orelse not strict then
     make_target ((serial1, description),
-      ((merge (op =) (reserved1, reserved2), Symtab.merge (K true) (includes1, includes2)),
+      ((merge (op =) (reserved1, reserved2), Symtab.join (K snd) (includes1, includes2)),
         (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
-          Symtab.join (K fst) (module_alias1, module_alias2))
+          Symtab.join (K snd) (module_alias1, module_alias2))
     ))
   else
     error ("Incompatible targets: " ^ quote target);