# HG changeset patch
# User nipkow
# Date 1080910031 -7200
# Node ID 9d8978a2ae569d782abf5ed526afb9e464bf0d6d
# Parent  859b11514537c3f9e37e5080349ebff26312fa04
got rid of ignore_neq again.

diff -r 859b11514537 -r 9d8978a2ae56 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Fri Apr 02 14:08:30 2004 +0200
+++ b/src/HOL/arith_data.ML	Fri Apr 02 14:47:11 2004 +0200
@@ -231,12 +231,6 @@
   {splits = splits, inj_consts = c :: inj_consts, discrete = discrete, presburger = presburger});
 
 
-(* A FIXME to avoid excessive case splits when ~= is split into < and >:
-   ignore ~= altogether.
-*)
-
-val ignore_neq = ref false;
-
 structure LA_Data_Ref: LIN_ARITH_DATA =
 struct
 
@@ -339,8 +333,7 @@
      | _       => None
   end handle Zero => None;
 
-fun negate(Some(x,i,rel,y,j,d)) =
-      if rel = "=" andalso !ignore_neq then None else Some(x,i,"~"^rel,y,j,d)
+fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d)
   | negate None = None;
 
 fun decomp1 (discrete,inj_consts) (T,xxx) =
@@ -435,14 +428,10 @@
 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))))
-   (elim_neq_tac THEN' fast_ex_arith_tac ex)
-   i st
-  end;
+   ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_ex_arith_tac ex)
+   i st;
 
 fun presburger_tac i st =
   (case ArithTheoryData.get_sg (sign_of_thm st) of