--- a/src/HOL/Tools/transfer.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/transfer.ML Tue Oct 20 16:13:01 2009 +0200
@@ -143,7 +143,7 @@
{inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2,
ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
hints = subtract (op = : string*string -> bool) hints0
- (hints1 union_string hints2)}
+ (gen_union (op =) (hints1, hints2))}
end;
local
@@ -151,7 +151,7 @@
in
fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
{inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) =
- {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = hints1 union_string hints2}
+ {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = gen_union (op =) (hints1, hints2)}
end;
fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =