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;
authorwenzelm
Thu Jun 24 14:31:01 2010 +0200 (2010-06-24)
changeset 3752842804fb5dd92
parent 37527 d9c2fdd6614f
child 37529 a23e8aa853eb
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;
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_target.ML	Thu Jun 24 14:19:08 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Thu Jun 24 14:31:01 2010 +0200
     1.3 @@ -142,9 +142,9 @@
     1.4        name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
     1.5    if serial1 = serial2 orelse not strict then
     1.6      make_target ((serial1, serializer),
     1.7 -      ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),
     1.8 +      ((merge (op =) (reserved1, reserved2), Symtab.merge (K true) (includes1, includes2)),
     1.9          (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
    1.10 -          Symtab.join (K snd) (module_alias1, module_alias2))
    1.11 +          Symtab.join (K fst) (module_alias1, module_alias2))
    1.12      ))
    1.13    else
    1.14      error ("Incompatible serializers: " ^ quote target);