diff -r 9d8978a2ae56 -r 73ea1234bb23 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Fri Apr 02 14:47:11 2004 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Apr 02 14:48:31 2004 +0200
@@ -77,6 +77,7 @@
                      lessD: thm list, simpset: Simplifier.simpset})
                 -> theory -> theory
   val trace           : bool ref
+  val fast_arith_neq_limit: int ref
   val lin_arith_prover: Sign.sg -> thm list -> term -> thm option
   val     lin_arith_tac:     bool -> int -> tactic
   val cut_lin_arith_tac: thm list -> int -> tactic
@@ -620,9 +621,19 @@
     end
     state;
 
+fun count P xs = length(filter P xs);
+
+(* The limit on the number of ~= allowed.
+   Because each ~= is split into two cases, this can lead to an explosion.
+*)
+val fast_arith_neq_limit = ref 9;
+
 fun prove sg ps ex Hs concl =
 let val Hitems = map (LA_Data.decomp sg) Hs
-in case LA_Data.decomp sg concl of
+in if count (fn None => false | Some(_,_,r,_,_,_) => r = "~=") Hitems
+      > !fast_arith_neq_limit then None
+   else
+   case LA_Data.decomp sg concl of
      None => refute sg ps ex (Hitems@[None])
    | Some(citem as (r,i,rel,l,j,d)) =>
        let val neg::rel0 = explode rel