# HG changeset patch
# User berghofe
# Date 1143197647 -3600
# Node ID 659b8165c7248e1ef46ed7700b983fc81764d02f
# Parent  ec5cd5b1804c9d5ea041eb3ad38063560c69fe75
Removed occurrences of makestring, which does not
exist in SML/NJ.

diff -r ec5cd5b1804c -r 659b8165c724 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Thu Mar 23 20:03:53 2006 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Mar 24 11:54:07 2006 +0100
@@ -591,8 +591,7 @@
 fun refutes sg (pTs,params) ex =
 let
   fun refute (initems::initemss) js =
-    let val _ = trace_msg ("initems: " ^ makestring initems)  (* TODO *)
-        val atoms = Library.foldl add_atoms ([],initems)
+    let val atoms = Library.foldl add_atoms ([],initems)
         val n = length atoms
         val mkleq = mklineq n atoms
         val ixs = 0 upto (n-1)
@@ -632,7 +631,6 @@
 
 fun prove sg ps ex Hs concl =
 let val Hitems = map (LA_Data.decomp sg) Hs
-    val _ = trace_msg ("Hitems: " ^ makestring Hitems)  (* TODO *)
 in if count (fn NONE => false | SOME(_,_,r,_,_,_) => r = "~=") Hitems
       > !fast_arith_neq_limit then NONE
    else