--- 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;