join entries properly on theory merge

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