# HG changeset patch
# User chaieb
# Date 1235135697 0
# Node ID 7d97e20728d44bbbac8fdfbb5c072e927c82fdf9
# Parent  dd27e16677b20982ed286d2948f66a5a7e9239d3# Parent  6ddb5a1690d9795c463c6c3cee96bf36287b82f4
merged

diff -r dd27e16677b2 -r 7d97e20728d4 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Thu Feb 19 23:18:28 2009 -0800
+++ b/src/HOL/Tools/Qelim/presburger.ML	Fri Feb 20 13:14:57 2009 +0000
@@ -170,14 +170,14 @@
   THEN_ALL_NEW simp_tac ss
   THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
   THEN_ALL_NEW ObjectLogic.full_atomize_tac
-  THEN_ALL_NEW (TRY o thin_prems_tac (is_relevant ctxt))
+  THEN_ALL_NEW (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 core_cooper_tac ctxt
+  THEN_ALL_NEW (core_cooper_tac ctxt)
   THEN_ALL_NEW finish_tac elim
 end;