# HG changeset patch # User chaieb # Date 1234907508 0 # Node ID 6ddb5a1690d9795c463c6c3cee96bf36287b82f4 # Parent 7a2eb84343f941404c2651f171459ce0e8ea7699# Parent 615ac9dc48b1766f3568de5161fdfd220d244fc0 merged diff -r 7a2eb84343f9 -r 6ddb5a1690d9 src/HOL/Tools/Qelim/presburger.ML --- a/src/HOL/Tools/Qelim/presburger.ML Tue Feb 17 21:51:52 2009 +0100 +++ b/src/HOL/Tools/Qelim/presburger.ML Tue Feb 17 21:51:48 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;