diff -r 45c9fc22904b -r cf1c19eee826 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Mar 22 11:14:58 2006 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Mar 22 11:54:54 2006 +0100
@@ -23,7 +23,7 @@
 
 signature LIN_ARITH_LOGIC =
 sig
-  val conjI:		thm
+  val conjI:		thm (* P ==> Q ==> P & Q *)
   val ccontr:           thm (* (~ P ==> False) ==> P *)
   val notI:             thm (* (P ==> False) ==> ~ P *)
   val not_lessD:        thm (* ~(m < n) ==> n <= m *)
@@ -76,7 +76,7 @@
                  -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
                      lessD: thm list, neqE: thm list, simpset: Simplifier.simpset})
                 -> theory -> theory
-  val trace           : bool ref
+  val trace: bool ref
   val fast_arith_neq_limit: int ref
   val lin_arith_prover: theory -> simpset -> term -> thm option
   val     lin_arith_tac:    bool -> int -> tactic
@@ -591,7 +591,8 @@
 fun refutes sg (pTs,params) ex =
 let
   fun refute (initems::initemss) js =
-    let val atoms = Library.foldl add_atoms ([],initems)
+    let val _ = trace_msg ("initems: " ^ makestring initems)  (* TODO *)
+        val atoms = Library.foldl add_atoms ([],initems)
         val n = length atoms
         val mkleq = mklineq n atoms
         val ixs = 0 upto (n-1)
@@ -631,6 +632,7 @@
 
 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