prefer first constant component on merge
authorhaftmann
Mon Oct 15 15:29:41 2007 +0200 (2007-10-15 ago)
changeset 25037d6a3dec2375d
parent 25036 6394db28d795
child 25038 522abf8a5f87
prefer first constant component on merge
src/Pure/consts.ML
     1.1 --- a/src/Pure/consts.ML	Mon Oct 15 15:29:39 2007 +0200
     1.2 +++ b/src/Pure/consts.ML	Mon Oct 15 15:29:41 2007 +0200
     1.3 @@ -208,11 +208,6 @@
     1.4  fun err_dup_const c =
     1.5    error ("Duplicate declaration of constant " ^ quote c);
     1.6  
     1.7 -fun err_inconsistent_constraints (constr1 : typ Symtab.table, constr2 : typ Symtab.table) c =
     1.8 -  error ("Inconsistent type constraints for constant " ^ quote c ^ "\n"
     1.9 -    ^ (setmp show_sorts true makestring o the o Symtab.lookup constr1) c ^ "\n"
    1.10 -    ^ (setmp show_sorts true makestring o the o Symtab.lookup constr2) c); (*FIXME*)
    1.11 -
    1.12  fun extend_decls naming decl tab = NameSpace.extend_table naming [decl] tab
    1.13    handle Symtab.DUP c => err_dup_const c;
    1.14  
    1.15 @@ -306,8 +301,7 @@
    1.16    let
    1.17      val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2)
    1.18        handle Symtab.DUP c => err_dup_const c;
    1.19 -    val constraints' = (*Symtab.merge (op =)*)Symtab.join (K snd)(*FIXME*) (constraints1, constraints2)
    1.20 -      handle Symtab.DUP c => err_inconsistent_constraints (constraints1, constraints2) c;
    1.21 +    val constraints' = Symtab.join (K fst) (constraints1, constraints2);
    1.22      val rev_abbrevs' = (rev_abbrevs1, rev_abbrevs2) |> Symtab.join
    1.23        (K (Library.merge (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u')));
    1.24    in make_consts (decls', constraints', rev_abbrevs') end;