# HG changeset patch
# User chaieb
# Date 1199352454 -3600
# Node ID 0298341876d0cc49aaec657145b1841f8119afb6
# Parent  7a204e0467f83d2c94c61f780912174bd46e1e4c
Changed order of tactics in presburger --- thinning before case splits

diff -r 7a204e0467f8 -r 0298341876d0 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Thu Jan 03 00:15:42 2008 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML	Thu Jan 03 10:27:34 2008 +0100
@@ -170,13 +170,13 @@
   THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
   THEN_ALL_NEW simp_tac ss
   THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
+  THEN_ALL_NEW (TRY o thin_prems_tac (is_relevant ctxt))
   THEN_ALL_NEW ObjectLogic.full_atomize_tac
   THEN_ALL_NEW div_mod_tac ctxt
   THEN_ALL_NEW splits_tac ctxt
   THEN_ALL_NEW simp_tac ss
   THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
   THEN_ALL_NEW nat_to_int_tac ctxt
-  THEN_ALL_NEW (TRY o thin_prems_tac (is_relevant ctxt))
   THEN_ALL_NEW core_cooper_tac ctxt
   THEN_ALL_NEW finish_tac elim
 end;