diff -r b22e44496dc2 -r 8f9594c31de4 src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Tue Oct 20 16:13:01 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Wed Oct 21 08:14:38 2009 +0200
@@ -364,7 +364,7 @@
 fun replace_dep (old:int, new) dep = if dep=old then new else [dep];
 
 fun replace_deps (old:int, new) (lno, t, deps) =
-      (lno, t, List.foldl (gen_union (op =)) [] (map (replace_dep (old, new)) deps));
+      (lno, t, List.foldl (union (op =)) [] (map (replace_dep (old, new)) deps));
 
 (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
   only in type information.*)