--- a/src/Pure/consts.ML Tue Jan 08 10:34:19 2013 +0100
+++ b/src/Pure/consts.ML Tue Jan 08 12:39:39 2013 +0100
@@ -318,7 +318,7 @@
Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
let
val decls' = Name_Space.merge_tables (decls1, decls2);
- val constraints' = Symtab.join (K fst) (constraints1, constraints2);
+ val constraints' = Symtab.merge (K true) (constraints1, constraints2);
val rev_abbrevs' = Symtab.join (K Item_Net.merge) (rev_abbrevs1, rev_abbrevs2);
in make_consts (decls', constraints', rev_abbrevs') end;