--- a/src/Provers/Arith/fast_lin_arith.ML Sat May 19 11:33:30 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Sat May 19 11:33:31 2007 +0200
@@ -219,7 +219,7 @@
then if exactl then lb else ratmiddle (lb, ub)
else if exactu then ub else ratmiddle (lb, ub)
else (*discrete domain, both bounds must be exact*)
- if ord = GREATER (*FIXME this is apparently nonsense*)
+ if ord = GREATER
then let val lb' = Rat.roundup lb in
if Rat.le lb' ub then lb' else raise NoEx end
else let val ub' = Rat.rounddown ub in