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