--- a/src/Pure/skip_proof.ML Tue Feb 10 14:29:36 2015 +0100
+++ b/src/Pure/skip_proof.ML Tue Feb 10 14:48:26 2015 +0100
@@ -12,7 +12,7 @@
val report: Proof.context -> unit
val make_thm_cterm: cterm -> thm
val make_thm: theory -> term -> thm
- val cheat_tac: int -> tactic
+ val cheat_tac: Proof.context -> int -> tactic
end;
structure Skip_Proof: SKIP_PROOF =
@@ -37,7 +37,7 @@
(* cheat_tac *)
-fun cheat_tac i st =
- resolve_tac [make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))] i st;
+fun cheat_tac ctxt i st =
+ resolve_tac ctxt [make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))] i st;
end;