src/HOL/Tools/Qelim/presburger.ML
changeset 35625 9c818cab0dd0
parent 35410 1ea89d2a1bd4
child 36692 54b64d4ad524
child 36714 ae84ddf03c58
     1.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -166,13 +166,13 @@
     1.4      val aprems = Arith_Data.get_arith_facts ctxt
     1.5  in
     1.6    Method.insert_tac aprems
     1.7 -  THEN_ALL_NEW ObjectLogic.full_atomize_tac
     1.8 +  THEN_ALL_NEW Object_Logic.full_atomize_tac
     1.9    THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
    1.10    THEN_ALL_NEW simp_tac ss
    1.11    THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
    1.12 -  THEN_ALL_NEW ObjectLogic.full_atomize_tac
    1.13 +  THEN_ALL_NEW Object_Logic.full_atomize_tac
    1.14    THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
    1.15 -  THEN_ALL_NEW ObjectLogic.full_atomize_tac
    1.16 +  THEN_ALL_NEW Object_Logic.full_atomize_tac
    1.17    THEN_ALL_NEW div_mod_tac ctxt
    1.18    THEN_ALL_NEW splits_tac ctxt
    1.19    THEN_ALL_NEW simp_tac ss