# HG changeset patch
# User wenzelm
# Date 1512740392 -3600
# Node ID b762ed417ed90cbb51c8706c92e97bce556db8bb
# Parent  f37bf261bdf6897b8586a87e1f2667801f5e09d3
implicit quick_and_dirty as for Toplevel.begin_proof/Proof.global_skip_proof;

diff -r f37bf261bdf6 -r b762ed417ed9 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Dec 07 18:44:04 2017 +0000
+++ b/src/Pure/Isar/proof.ML	Fri Dec 08 14:39:52 2017 +0100
@@ -1151,7 +1151,7 @@
   in
     if Goal.skip_proofs_enabled () andalso not (is_relevant state) then
       state
-      |> proof (SOME (Method.sorry_text false, #2 initial'))
+      |> proof (SOME (Method.sorry_text true, #2 initial'))
       |> Seq.maps_results (qeds (#2 (#2 initial), (NONE, #2 terminal)))
     else
       state