src/Provers/Arith/fast_lin_arith.ML
changeset 33037 b22e44496dc2
parent 33002 f3f02f36a3e2
child 33038 8f9594c31de4
     1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -385,7 +385,7 @@
     1.4    let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
     1.5    if not (null eqs) then
     1.6       let val c =
     1.7 -           fold (fn Lineq(_,_,l,_) => fn cs => l union cs) eqs []
     1.8 +           fold (fn Lineq(_,_,l,_) => fn cs => gen_union (op =) (l, cs)) eqs []
     1.9             |> filter (fn i => i <> 0)
    1.10             |> sort (int_ord o pairself abs)
    1.11             |> hd