# HG changeset patch
# User nipkow
# Date 1080900518 -7200
# Node ID 6807f524ac4da2adb383fc3003923721ce541d87
# Parent  e2373489d3739c3a08898c55ca11f1908e980c4d
Added ignore_neq flag.

diff -r e2373489d373 -r 6807f524ac4d src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Thu Apr 01 15:05:04 2004 +0200
+++ b/src/HOL/arith_data.ML	Fri Apr 02 12:08:38 2004 +0200
@@ -231,6 +231,12 @@
   {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
 
@@ -333,7 +339,8 @@
      | _       => None
   end handle Zero => None;
 
-fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d)
+fun negate(Some(x,i,rel,y,j,d)) =
+      if rel = "=" andalso !ignore_neq then None else Some(x,i,"~"^rel,y,j,d)
   | negate None = None;
 
 fun decomp1 (discrete,inj_consts) (T,xxx) =