# HG changeset patch
# User nipkow
# Date 1080901548 -7200
# Node ID 0af3da3beae83525b01e05ac08e8d614802ae608
# Parent  6807f524ac4da2adb383fc3003923721ce541d87
ignore_neq also influences arith_tac now, not just fast_arith_tac

diff -r 6807f524ac4d -r 0af3da3beae8 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Fri Apr 02 12:08:38 2004 +0200
+++ b/src/HOL/arith_data.ML	Fri Apr 02 12:25:48 2004 +0200
@@ -435,10 +435,14 @@
 local
 
 fun raw_arith_tac ex i st =
+  let fun elim_neq_tac i =
+      COND (K(!ignore_neq)) all_tac (REPEAT_DETERM(etac linorder_neqE i))
+  in
   refute_tac (K true)
    (REPEAT o split_tac (#splits (ArithTheoryData.get_sg (Thm.sign_of_thm st))))
-   ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_ex_arith_tac ex)
-   i st;
+   (elim_neq_tac THEN' fast_ex_arith_tac ex)
+   i st
+  end;
 
 fun presburger_tac i st =
   (case ArithTheoryData.get_sg (sign_of_thm st) of