src/Pure/Isar/proof.ML
changeset 67161 b762ed417ed9
parent 67157 d0657c8b7616
child 67522 9e712280cc37
equal deleted inserted replaced
67160:f37bf261bdf6 67161:b762ed417ed9
  1149     val initial' = apfst check_closure initial;
  1149     val initial' = apfst check_closure initial;
  1150     val terminal' = (apfst o Option.map o apfst) check_closure terminal;
  1150     val terminal' = (apfst o Option.map o apfst) check_closure terminal;
  1151   in
  1151   in
  1152     if Goal.skip_proofs_enabled () andalso not (is_relevant state) then
  1152     if Goal.skip_proofs_enabled () andalso not (is_relevant state) then
  1153       state
  1153       state
  1154       |> proof (SOME (Method.sorry_text false, #2 initial'))
  1154       |> proof (SOME (Method.sorry_text true, #2 initial'))
  1155       |> Seq.maps_results (qeds (#2 (#2 initial), (NONE, #2 terminal)))
  1155       |> Seq.maps_results (qeds (#2 (#2 initial), (NONE, #2 terminal)))
  1156     else
  1156     else
  1157       state
  1157       state
  1158       |> proof (SOME initial')
  1158       |> proof (SOME initial')
  1159       |> Seq.maps_results (qeds (#2 (#2 initial), terminal'))
  1159       |> Seq.maps_results (qeds (#2 (#2 initial), terminal'))