# HG changeset patch
# User nipkow
# Date 1120732970 -7200
# Node ID 008d089822e35ff6127dc45fa2ce0aebb22ef6cd
# Parent  2c76db916c51cb24539039bab2b06313fdfc38b5
takes & in premises apart now.

diff -r 2c76db916c51 -r 008d089822e3 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Thu Jul 07 12:42:21 2005 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Jul 07 12:42:50 2005 +0200
@@ -30,6 +30,7 @@
   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
@@ -731,7 +732,7 @@
 *)
 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? *)