src/Provers/Arith/cancel_numerals.ML
changeset 58838 59203adfc33f
parent 54565 63e4474fd0ed
child 59498 50b60f501b05
     1.1 --- a/src/Provers/Arith/cancel_numerals.ML	Thu Oct 30 16:20:46 2014 +0100
     1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Thu Oct 30 16:55:29 2014 +0100
     1.3 @@ -92,12 +92,12 @@
     1.4      Option.map (export o Data.simplify_meta_eq ctxt)
     1.5        (if n2 <= n1 then
     1.6           Data.prove_conv
     1.7 -           [Data.trans_tac reshape, rtac Data.bal_add1 1,
     1.8 +           [Data.trans_tac reshape, resolve_tac [Data.bal_add1] 1,
     1.9              Data.numeral_simp_tac ctxt] ctxt prems
    1.10             (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2'))
    1.11         else
    1.12           Data.prove_conv
    1.13 -           [Data.trans_tac reshape, rtac Data.bal_add2 1,
    1.14 +           [Data.trans_tac reshape, resolve_tac [Data.bal_add2] 1,
    1.15              Data.numeral_simp_tac ctxt] ctxt prems
    1.16             (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2'))))
    1.17    end