# HG changeset patch
# User haftmann
# Date 1192192949 -7200
# Node ID 7982fe02a50edbb893350df946fdead0cebdc1ec
# Parent  1ab44e69652fe309a602172a35a36369db1b3ec8
(intermediate quickfix)

diff -r 1ab44e69652f -r 7982fe02a50e src/Pure/consts.ML
--- a/src/Pure/consts.ML	Fri Oct 12 10:29:02 2007 +0200
+++ b/src/Pure/consts.ML	Fri Oct 12 14:42:29 2007 +0200
@@ -195,7 +195,7 @@
 
 fun instance consts (c, Ts) =
   let
-    val declT = the_declaration consts c;
+    val ({ T = declT, ... }, _) = the_const consts c;
     val vars = map Term.dest_TVar (typargs consts (c, declT));
     val inst = vars ~~ Ts handle UnequalLengths =>
       raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
@@ -208,8 +208,10 @@
 fun err_dup_const c =
   error ("Duplicate declaration of constant " ^ quote c);
 
-fun err_inconsistent_constraints c =
-  error ("Inconsistent type constraints for 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;
@@ -304,8 +306,8 @@
   let
     val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2)
       handle Symtab.DUP c => err_dup_const c;
-    val constraints' = Symtab.merge (op =) (constraints1, constraints2)
-      handle Symtab.DUP c => err_inconsistent_constraints c;
+    val constraints' = (*Symtab.merge (op =)*)Symtab.join (K snd)(*FIXME*) (constraints1, constraints2)
+      handle Symtab.DUP c => err_inconsistent_constraints (constraints1, constraints2) c;
     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;