src/HOL/Tools/res_reconstruct.ML
changeset 33037 b22e44496dc2
parent 32994 ccc07fbbfefd
child 33038 8f9594c31de4
     1.1 --- a/src/HOL/Tools/res_reconstruct.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -364,7 +364,7 @@
     1.4  fun replace_dep (old:int, new) dep = if dep=old then new else [dep];
     1.5  
     1.6  fun replace_deps (old:int, new) (lno, t, deps) =
     1.7 -      (lno, t, List.foldl (op union_int) [] (map (replace_dep (old, new)) deps));
     1.8 +      (lno, t, List.foldl (gen_union (op =)) [] (map (replace_dep (old, new)) deps));
     1.9  
    1.10  (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
    1.11    only in type information.*)