# HG changeset patch
# User hoelzl
# Date 1268148643 -3600
# Node ID d58a4ac1ca1c9eacc315aaa252f0f99b177eeae8
# Parent  f1315bbf1bc9b91d27b59142e2b9a3b72d7f9538
Use same order of neq-elimination as in proof search.

diff -r f1315bbf1bc9 -r d58a4ac1ca1c src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Mon Mar 08 11:30:55 2010 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Mar 09 16:30:43 2010 +0100
@@ -849,17 +849,20 @@
 
 fun splitasms ctxt (asms : thm list) : splittree =
 let val {neqE, ...} = get_data ctxt
-    fun elim_neq (asms', []) = Tip (rev asms')
-      | elim_neq (asms', asm::asms) =
-      (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) neqE of
+    fun elim_neq [] (asms', []) = Tip (rev asms')
+      | elim_neq [] (asms', asms) = Tip (rev asms' @ asms)
+      | elim_neq (neq :: neqs) (asms', []) = elim_neq neqs ([],rev asms')
+      | elim_neq (neqs as (neq :: _)) (asms', asm::asms) =
+      (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) [neq] of
         SOME spl =>
           let val (ct1, ct2) = extract (cprop_of spl)
               val thm1 = assume ct1
               val thm2 = assume ct2
-          in Spl (spl, ct1, elim_neq (asms', asms@[thm1]), ct2, elim_neq (asms', asms@[thm2]))
+          in Spl (spl, ct1, elim_neq neqs (asms', asms@[thm1]),
+            ct2, elim_neq neqs (asms', asms@[thm2]))
           end
-      | NONE => elim_neq (asm::asms', asms))
-in elim_neq ([], asms) end;
+      | NONE => elim_neq neqs (asm::asms', asms))
+in elim_neq neqE ([], asms) end;
 
 fun fwdproof ss (Tip asms : splittree) (j::js : injust list) = (mkthm ss asms j, js)
   | fwdproof ss (Spl (thm, ct1, tree1, ct2, tree2)) js =