# HG changeset patch # User haftmann # Date 1256812899 -3600 # Node ID 28e3ce50a5a16703f1661153a5a2a9fd6344d2e4 # Parent 73998ef6ea91111051ee2733eadeb994cd474cff join entries properly on theory merge diff -r 73998ef6ea91 -r 28e3ce50a5a1 src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Thu Oct 29 11:41:38 2009 +0100 +++ b/src/HOL/Tools/transfer.ML Thu Oct 29 11:41:39 2009 +0100 @@ -14,8 +14,15 @@ structure Transfer : TRANSFER = struct -type entry = {inj : thm list, emb : thm list, ret : thm list, cong : thm list, - guess : bool, hints : string list}; +type entry = { inj : thm list, emb : thm list, ret : thm list, cong : thm list, + guess : bool, hints : string list }; + +fun merge_entry ({ inj = inj1, emb = emb1, ret = ret1, cong = cong1, guess = guess1, hints = hints1 } : entry, + { inj = inj2, emb = emb2, ret = ret2, cong = cong2, guess = guess2, hints = hints2 } : entry) = + { inj = merge Thm.eq_thm (inj1, inj2), emb = merge Thm.eq_thm (emb1, emb2), + ret = merge Thm.eq_thm (ret1, ret2), cong = merge Thm.eq_thm (cong1, cong2), + guess = guess1 andalso guess2, hints = merge (op =) (hints1, hints2) }; + type data = simpset * (thm * entry) list; structure Data = GenericDataFun @@ -24,7 +31,7 @@ val empty = (HOL_ss, []); val extend = I; fun merge _ ((ss1, e1), (ss2, e2)) = - (merge_ss (ss1, ss2), AList.merge Thm.eq_thm (K true) (e1, e2)); + (merge_ss (ss1, ss2), AList.join Thm.eq_thm (K merge_entry) (e1, e2)); ); val get = Data.get o Context.Proof;