diff -r 0c5cd369a643 -r 50b60f501b05 src/Pure/skip_proof.ML
--- 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;