src/HOL/Tools/Qelim/cooper.ML
changeset 54742 7a86358a3c0b
parent 54489 03ff4d1e6784
child 54883 dd04a8b654fc
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -865,19 +865,19 @@
     1.4      val aprems = Arith_Data.get_arith_facts ctxt
     1.5    in
     1.6      Method.insert_tac aprems
     1.7 -    THEN_ALL_NEW Object_Logic.full_atomize_tac
     1.8 +    THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
     1.9      THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
    1.10      THEN_ALL_NEW simp_tac simpset_ctxt
    1.11      THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
    1.12 -    THEN_ALL_NEW Object_Logic.full_atomize_tac
    1.13 +    THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
    1.14      THEN_ALL_NEW (thin_prems_tac ctxt (is_relevant ctxt))
    1.15 -    THEN_ALL_NEW Object_Logic.full_atomize_tac
    1.16 +    THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
    1.17      THEN_ALL_NEW div_mod_tac ctxt
    1.18      THEN_ALL_NEW splits_tac ctxt
    1.19      THEN_ALL_NEW simp_tac simpset_ctxt
    1.20      THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
    1.21      THEN_ALL_NEW nat_to_int_tac ctxt
    1.22 -    THEN_ALL_NEW (core_tac ctxt)
    1.23 +    THEN_ALL_NEW core_tac ctxt
    1.24      THEN_ALL_NEW finish_tac elim
    1.25    end 1);
    1.26