1.1 --- a/src/Provers/Arith/combine_numerals.ML	Sat Sep 17 00:40:27 2011 +0200
     1.2 +++ b/src/Provers/Arith/combine_numerals.ML	Sat Sep 17 15:08:55 2011 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4    val left_distrib: thm
     1.5    (*proof tools*)
     1.6    val prove_conv: tactic list -> Proof.context -> term * term -> thm option
     1.7 -  val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
     1.8 +  val trans_tac: thm option -> tactic            (*applies the initial lemma*)
     1.9    val norm_tac: simpset -> tactic                (*proves the initial lemma*)
    1.10    val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
    1.11    val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
    1.12 @@ -83,7 +83,7 @@
    1.13    in
    1.14      Option.map (export o Data.simplify_meta_eq ss)
    1.15        (Data.prove_conv
    1.16 -         [Data.trans_tac ss reshape, rtac Data.left_distrib 1,
    1.17 +         [Data.trans_tac reshape, rtac Data.left_distrib 1,
    1.18            Data.numeral_simp_tac ss] ctxt
    1.19           (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
    1.20    end