--- a/src/Tools/cong_tac.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Tools/cong_tac.ML Sun Nov 09 14:08:00 2014 +0100
@@ -6,13 +6,13 @@
signature CONG_TAC =
sig
- val cong_tac: thm -> int -> tactic
+ val cong_tac: Proof.context -> thm -> int -> tactic
end;
structure Cong_Tac: CONG_TAC =
struct
-fun cong_tac cong = CSUBGOAL (fn (cgoal, i) =>
+fun cong_tac ctxt cong = CSUBGOAL (fn (cgoal, i) =>
let
val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
val goal = Thm.term_of cgoal;
@@ -28,7 +28,7 @@
|> map (fn (t, u) => (cert (Term.head_of t), cert (fold_rev Term.abs ps u)));
in
fn st =>
- compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
+ compose_tac ctxt (false, Drule.cterm_instantiate insts cong', 2) i st
handle THM _ => no_tac st
end
| _ => no_tac)