diff -r 64469ea43735 -r 8ae418dfe561 src/Provers/Arith/combine_numerals.ML
--- a/src/Provers/Arith/combine_numerals.ML	Sat Sep 17 00:40:27 2011 +0200
+++ b/src/Provers/Arith/combine_numerals.ML	Sat Sep 17 15:08:55 2011 +0200
@@ -29,7 +29,7 @@
   val left_distrib: thm
   (*proof tools*)
   val prove_conv: tactic list -> Proof.context -> term * term -> thm option
-  val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
+  val trans_tac: thm option -> tactic            (*applies the initial lemma*)
   val norm_tac: simpset -> tactic                (*proves the initial lemma*)
   val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
   val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
@@ -83,7 +83,7 @@
   in
     Option.map (export o Data.simplify_meta_eq ss)
       (Data.prove_conv
-         [Data.trans_tac ss reshape, rtac Data.left_distrib 1,
+         [Data.trans_tac reshape, rtac Data.left_distrib 1,
           Data.numeral_simp_tac ss] ctxt
          (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
   end