Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Provers/Arith/combine_numerals.ML
changeset 59498 50b60f501b05
parent 58838 59203adfc33f
child 59530 2a20354c0877 
--- a/src/Provers/Arith/combine_numerals.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/Provers/Arith/combine_numerals.ML	Tue Feb 10 14:48:26 2015 +0100
@@ -83,7 +83,7 @@
   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
isabelle