# HG changeset patch
# User wenzelm
# Date 1566040579 -7200
# Node ID 0c1b08d0b1fe8e5775c35ca4305d99e49ecdd00c
# Parent  7714971a58b56ea04142f68f0c771c788480825e
more accurate proposition for cheat_tac (command 'sorry');

diff -r 7714971a58b5 -r 0c1b08d0b1fe src/Pure/skip_proof.ML
--- 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;