src/Provers/Arith/combine_numerals.ML
changeset 58838 59203adfc33f
parent 51717 9e7d1c139569
child 59498 50b60f501b05
     1.1 --- a/src/Provers/Arith/combine_numerals.ML	Thu Oct 30 16:20:46 2014 +0100
     1.2 +++ b/src/Provers/Arith/combine_numerals.ML	Thu Oct 30 16:55:29 2014 +0100
     1.3 @@ -83,7 +83,7 @@
     1.4    in
     1.5      Option.map (export o Data.simplify_meta_eq ctxt)
     1.6        (Data.prove_conv
     1.7 -         [Data.trans_tac reshape, rtac Data.left_distrib 1,
     1.8 +         [Data.trans_tac reshape, resolve_tac [Data.left_distrib] 1,
     1.9            Data.numeral_simp_tac ctxt] ctxt
    1.10           (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
    1.11    end