# 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