--- a/src/Pure/skip_proof.ML Sat Aug 17 12:44:22 2019 +0200
+++ b/src/Pure/skip_proof.ML Sat Aug 17 13:16:19 2019 +0200
@@ -34,7 +34,12 @@
(* cheat_tac *)
-fun cheat_tac ctxt i st =
- resolve_tac ctxt [make_thm (Proof_Context.theory_of ctxt) (Var (("A", 0), propT))] i st;
+fun cheat_tac ctxt = SUBGOAL (fn (goal, i) =>
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val assms = Assumption.all_assms_of ctxt;
+ val cheat = make_thm thy (Logic.list_implies (map Thm.term_of assms, goal));
+ val thm = Drule.implies_elim_list cheat (map Thm.assume assms);
+ in PRIMITIVE (Drule.with_subgoal i (Thm.elim_implies thm)) end);
end;