| changeset 60820 | d0a88a2182a8 |
| parent 59621 | 291934bac95e |
| child 61527 | d05f3d86a758 |
--- 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;