implicit quick_and_dirty as for Toplevel.begin_proof/Proof.global_skip_proof;
authorwenzelm
Fri Dec 08 14:39:52 2017 +0100 (17 months ago)
changeset 67161b762ed417ed9
parent 67160 f37bf261bdf6
child 67162 0050cd50936d
implicit quick_and_dirty as for Toplevel.begin_proof/Proof.global_skip_proof;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Dec 07 18:44:04 2017 +0000
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri Dec 08 14:39:52 2017 +0100
     1.3 @@ -1151,7 +1151,7 @@
     1.4    in
     1.5      if Goal.skip_proofs_enabled () andalso not (is_relevant state) then
     1.6        state
     1.7 -      |> proof (SOME (Method.sorry_text false, #2 initial'))
     1.8 +      |> proof (SOME (Method.sorry_text true, #2 initial'))
     1.9        |> Seq.maps_results (qeds (#2 (#2 initial), (NONE, #2 terminal)))
    1.10      else
    1.11        state