--- 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