src/Provers/Arith/fast_lin_arith.ML

            fold (fn Lineq(_,_,l,_) => fn cs => union (op =) l cs) eqs []
            |> filter (fn i => i <> 0)
            |> sort (int_ord o pairself abs)
            |> hd
          val (eq as Lineq(_,_,ceq,_),othereqs) =
-               extract_first (fn Lineq(_,_,l,_) => c mem l) eqs
+               extract_first (fn Lineq(_,_,l,_) => member (op =) l c) eqs
          val v = find_index (fn v => v = c) ceq
          val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0)
                                      (othereqs @ noneqs)
          val others = map (elim_var v eq) roth @ ioth
      in elim(others,(v,nontriv)::hist) end