src/Provers/Arith/fast_lin_arith.ML
changeset 59584 4517e9a96ace
parent 59582 0fbed69ff081
child 59586 ddf6deaadfe8
--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Mar 04 20:16:39 2015 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Mar 04 20:47:29 2015 +0100
@@ -404,7 +404,7 @@
   let val _ = print_ineqs ctxt ineqs
       val (triv, nontriv) = List.partition is_trivial ineqs in
   if not (null triv)
-  then case Library.find_first is_contradictory triv of
+  then case find_first is_contradictory triv of
          NONE => elim ctxt (nontriv, hist)
        | SOME(Lineq(_,_,_,j)) => Success j
   else