--- a/src/HOL/Tools/res_reconstruct.ML Wed Oct 21 12:02:19 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Wed Oct 21 12:02:56 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 (union (op =)) [] (map (replace_dep (old, new)) deps));
+ (lno, t, List.foldl (uncurry (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.*)