src/HOL/arith_data.ML

   {splits = splits, inj_consts = inj_consts, discrete = d :: discrete, presburger= presburger});
 
 fun arith_inj_const c = ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
   {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
 
 (* Decomposition of terms *)

      | "op <=" => Some(p,i,"<=",q,j)
      | "op ="  => Some(p,i,"=",q,j)
      | _       => 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) =
   (case T of
      Type("fun",[Type(D,[]),_]) =>