# HG changeset patch
# User nipkow
# Date 950964432 -3600
# Node ID 699d4ad2ced3e8324a3e31aba1e9329913d6b263
# Parent  08ad0a986db2c82280ea38add702035f229a9ba4
Commenst.

diff -r 08ad0a986db2 -r 699d4ad2ced3 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Fri Feb 18 20:27:19 2000 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Sat Feb 19 13:47:12 2000 +0100
@@ -194,13 +194,13 @@
         | extract xs []      = (None,xs)
   in extract [] end;
 
-
+(*?
 fun print_ineqs ineqs =
  writeln(cat_lines(""::map (fn Lineq(c,t,l,_) =>
    string_of_int c ^
    (case t of Eq => " =  " | Lt=> " <  " | Le => " <= ") ^
    commas(map string_of_int l)) ineqs));
-
+!*)
 
 fun elim ineqs =
   let (*?val dummy = print_ineqs ineqs;!*)