src/Provers/Arith/combine_numerals.ML

       else Data.prove_conv [Data.norm_tac ctxt] ctxt
         (t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms))
   in
     Option.map (export o Data.simplify_meta_eq ctxt)
       (Data.prove_conv
-         [Data.trans_tac reshape, resolve_tac [Data.left_distrib] 1,
+         [Data.trans_tac reshape, resolve_tac ctxt [Data.left_distrib] 1,
           Data.numeral_simp_tac ctxt] ctxt
          (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
   end
   (* FIXME avoid handling of generic exceptions *)
   handle TERM _ => NONE