implicit quick_and_dirty as for Toplevel.begin_proof/Proof.global_skip_proof;

--- 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