Removed occurrences of makestring, which does not
authorberghofe
Fri Mar 24 11:54:07 2006 +0100 (2006-03-24)
changeset 19324659b8165c724
parent 19323 ec5cd5b1804c
child 19325 35177b864f80
Removed occurrences of makestring, which does not
exist in SML/NJ.
src/Provers/Arith/fast_lin_arith.ML
     1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Thu Mar 23 20:03:53 2006 +0100
     1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Mar 24 11:54:07 2006 +0100
     1.3 @@ -591,8 +591,7 @@
     1.4  fun refutes sg (pTs,params) ex =
     1.5  let
     1.6    fun refute (initems::initemss) js =
     1.7 -    let val _ = trace_msg ("initems: " ^ makestring initems)  (* TODO *)
     1.8 -        val atoms = Library.foldl add_atoms ([],initems)
     1.9 +    let val atoms = Library.foldl add_atoms ([],initems)
    1.10          val n = length atoms
    1.11          val mkleq = mklineq n atoms
    1.12          val ixs = 0 upto (n-1)
    1.13 @@ -632,7 +631,6 @@
    1.14  
    1.15  fun prove sg ps ex Hs concl =
    1.16  let val Hitems = map (LA_Data.decomp sg) Hs
    1.17 -    val _ = trace_msg ("Hitems: " ^ makestring Hitems)  (* TODO *)
    1.18  in if count (fn NONE => false | SOME(_,_,r,_,_,_) => r = "~=") Hitems
    1.19        > !fast_arith_neq_limit then NONE
    1.20     else