1.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Tue Jul 03 15:23:11 2007 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Tue Jul 03 17:17:04 2007 +0200
     1.3 @@ -150,14 +150,14 @@
     1.4  let val ss = fst (CooperData.get ctxt) delsimps del_ths addsimps add_ths
     1.5  in
     1.6    ObjectLogic.full_atomize_tac
     1.7 -  THEN_ALL_NEW eta_long_tac
     1.8 +  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
     1.9    THEN_ALL_NEW simp_tac ss
    1.10    THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
    1.11    THEN_ALL_NEW ObjectLogic.full_atomize_tac
    1.12    THEN_ALL_NEW div_mod_tac ctxt
    1.13    THEN_ALL_NEW splits_tac ctxt
    1.14    THEN_ALL_NEW simp_tac ss
    1.15 -  THEN_ALL_NEW eta_long_tac
    1.16 +  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
    1.17    THEN_ALL_NEW nat_to_int_tac ctxt
    1.18    THEN_ALL_NEW (TRY o thin_prems_tac (is_relevant ctxt))
    1.19    THEN_ALL_NEW core_cooper_tac ctxt