# HG changeset patch
# User haftmann
# Date 1192454981 -7200
# Node ID d6a3dec2375d752bfa5f45cc9349cd7d65ff286d
# Parent  6394db28d7951392130763fa9254ff08bd62dd61
prefer first constant component on merge

diff -r 6394db28d795 -r d6a3dec2375d src/Pure/consts.ML
--- a/src/Pure/consts.ML	Mon Oct 15 15:29:39 2007 +0200
+++ b/src/Pure/consts.ML	Mon Oct 15 15:29:41 2007 +0200
@@ -208,11 +208,6 @@
 fun err_dup_const c =
   error ("Duplicate declaration of constant " ^ quote c);
 
-fun err_inconsistent_constraints (constr1 : typ Symtab.table, constr2 : typ Symtab.table) c =
-  error ("Inconsistent type constraints for constant " ^ quote c ^ "\n"
-    ^ (setmp show_sorts true makestring o the o Symtab.lookup constr1) c ^ "\n"
-    ^ (setmp show_sorts true makestring o the o Symtab.lookup constr2) c); (*FIXME*)
-
 fun extend_decls naming decl tab = NameSpace.extend_table naming [decl] tab
   handle Symtab.DUP c => err_dup_const c;
 
@@ -306,8 +301,7 @@
   let
     val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2)
       handle Symtab.DUP c => err_dup_const c;
-    val constraints' = (*Symtab.merge (op =)*)Symtab.join (K snd)(*FIXME*) (constraints1, constraints2)
-      handle Symtab.DUP c => err_inconsistent_constraints (constraints1, constraints2) c;
+    val constraints' = Symtab.join (K fst) (constraints1, constraints2);
     val rev_abbrevs' = (rev_abbrevs1, rev_abbrevs2) |> Symtab.join
       (K (Library.merge (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u')));
   in make_consts (decls', constraints', rev_abbrevs') end;