1.1 --- a/src/HOL/Tools/Qelim/presburger.ML Sun Feb 15 22:58:02 2009 +0100
1.2 +++ b/src/HOL/Tools/Qelim/presburger.ML Tue Feb 17 20:41:36 2009 +0000
1.3 @@ -170,14 +170,14 @@
1.4 THEN_ALL_NEW simp_tac ss
1.5 THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
1.6 THEN_ALL_NEW ObjectLogic.full_atomize_tac
1.7 - THEN_ALL_NEW (TRY o thin_prems_tac (is_relevant ctxt))
1.8 + THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
1.9 THEN_ALL_NEW ObjectLogic.full_atomize_tac
1.10 THEN_ALL_NEW div_mod_tac ctxt
1.11 THEN_ALL_NEW splits_tac ctxt
1.12 THEN_ALL_NEW simp_tac ss
1.13 THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
1.14 THEN_ALL_NEW nat_to_int_tac ctxt
1.15 - THEN_ALL_NEW core_cooper_tac ctxt
1.16 + THEN_ALL_NEW (core_cooper_tac ctxt)
1.17 THEN_ALL_NEW finish_tac elim
1.18 end;
1.19