# HG changeset patch
# User chaieb
# Date 1180943822 -7200
# Node ID b70c8c2283c2132570c56484154575bbdae693f6
# Parent  492e2fd127676d7e8797ced191576a21b28a2fbf
tuned;

diff -r 492e2fd12767 -r b70c8c2283c2 src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Sun Jun 03 23:16:57 2007 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Mon Jun 04 09:57:02 2007 +0200
@@ -318,23 +318,18 @@
     val simpset3 = HOL_basic_ss addsplits [abs_split]
     val ct = cterm_of sg (HOLogic.mk_Trueprop t)
     (* Theorem for the nat --> int transformation *)
-    val pre_thm = Seq.hd (EVERY
+    val pre_thm = Seq.hd ((EVERY o (map TRY)) 
       [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
-       TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
-       TRY (simp_tac simpset3 1), TRY (simp_tac presburger_ss 1)]
+       simp_tac simpset1 1, simp_tac simpset2 1,
+       simp_tac simpset3 1, simp_tac presburger_ss 1]
       (trivial ct))
     fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
     (* The result of the quantifier elimination *)
     val (th, tac) = case (prop_of pre_thm) of
         Const ("==>", _) $ (Const ("Trueprop", _) $ t1) $ _ =>
     let val pth =
-          (* If quick_and_dirty then run without proof generation as oracle*)
              if !quick_and_dirty
              then presburger_oracle sg (Pattern.eta_long [] t1)
-(*
-assume (cterm_of sg
-               (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1)))))
-*)
              else tmproof_of_int_qelim sg (Pattern.eta_long [] t1)
     in
           (trace_msg ("calling procedure with term:\n" ^