# HG changeset patch
# User wenzelm
# Date 1438106825 -7200
# Node ID d0a88a2182a80b972228ec1d98953fb522b7119b
# Parent  e1f1842bf344baa557c47459e48b09ae872b2d79
clarified context;

diff -r e1f1842bf344 -r d0a88a2182a8 src/Pure/skip_proof.ML
--- a/src/Pure/skip_proof.ML	Tue Jul 28 20:05:53 2015 +0200
+++ b/src/Pure/skip_proof.ML	Tue Jul 28 20:07:05 2015 +0200
@@ -38,6 +38,6 @@
 (* cheat_tac *)
 
 fun cheat_tac ctxt i st =
-  resolve_tac ctxt [make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))] i st;
+  resolve_tac ctxt [make_thm (Proof_Context.theory_of ctxt) (Var (("A", 0), propT))] i st;
 
 end;