Removed occurrences of makestring, which does not
authorberghofe
Fri, 24 Mar 2006 11:54:07 +0100
changeset 19324 659b8165c724
parent 19323 ec5cd5b1804c
child 19325 35177b864f80
Removed occurrences of makestring, which does not exist in SML/NJ.
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