src/Provers/Arith/fast_lin_arith.ML

   val notI:             thm (* (P ==> False) ==> ~ P *)
   val not_lessD:        thm (* ~(m < n) ==> n <= m *)
   val not_leD:          thm (* ~(m <= n) ==> n < m *)
   val sym:		thm (* x = y ==> y = x *)
   val mk_Eq: thm -> thm
+  val atomize: thm -> thm list
   val mk_Trueprop: term -> term
   val neg_prop: term -> term
   val is_False: thm -> bool
   val is_nat: typ list * term -> bool
   val mk_nat_thm: theory -> term -> thm

    2. lin_arith_prover is applied by the simplifier which
       dives into terms and will thus try the non-negated concl anyway.
 *)
 fun lin_arith_prover sg ss concl =
 let
-    val thms = prems_of_ss ss;
+    val thms = List.concat(map LA_Logic.atomize (prems_of_ss ss));
     val Hs = map (#prop o rep_thm) thms
     val Tconcl = LA_Logic.mk_Trueprop concl
 in case prove sg ([],[]) false Hs Tconcl of (* concl provable? *)
      SOME js => prover sg thms Tconcl js true
    | NONE => let val nTconcl = LA_Logic.neg_prop Tconcl