src/Provers/Arith/cancel_numerals.ML

   (*rules*)
   val bal_add1: thm
   val bal_add2: thm
   (*proof tools*)
   val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
-  val trans_tac: thm option -> tactic            (*applies the initial lemma*)
+  val trans_tac: Proof.context -> thm option -> tactic            (*applies the initial lemma*)
   val norm_tac: Proof.context -> tactic          (*proves the initial lemma*)
   val numeral_simp_tac: Proof.context -> tactic  (*proves the final theorem*)
   val simplify_meta_eq: Proof.context -> thm -> thm (*simplifies the final theorem*)
 end;
 

           (t', Data.mk_bal (newshape(n1,terms1'), newshape(n2,terms2')))
   in
     Option.map (export o Data.simplify_meta_eq ctxt)
       (if n2 <= n1 then
          Data.prove_conv
-           [Data.trans_tac reshape, resolve_tac ctxt [Data.bal_add1] 1,
+           [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.bal_add1] 1,
             Data.numeral_simp_tac ctxt] ctxt prems
            (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2'))
        else
          Data.prove_conv
-           [Data.trans_tac reshape, resolve_tac ctxt [Data.bal_add2] 1,
+           [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.bal_add2] 1,
             Data.numeral_simp_tac ctxt] ctxt prems
            (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2'))))
   end
   (* FIXME avoid handling of generic exceptions *)
   handle TERM _ => NONE