src/Pure/Isar/proof.ML
changeset 50912 8d391f185cac
parent 50885 f3588e59aeaa
child 51048 123be08eed88
equal deleted inserted replaced
50911:ee7fe4230642 50912:8d391f185cac
   825 fun end_proof bot (prev_pos, (opt_text, immed)) =
   825 fun end_proof bot (prev_pos, (opt_text, immed)) =
   826   let
   826   let
   827     val (finish_text, terminal_pos, finished_pos) =
   827     val (finish_text, terminal_pos, finished_pos) =
   828       (case opt_text of
   828       (case opt_text of
   829         NONE => (Method.finish_text (NONE, immed), Position.none, prev_pos)
   829         NONE => (Method.finish_text (NONE, immed), Position.none, prev_pos)
   830       | SOME (text, (pos, end_pos)) => (Method.finish_text (SOME text, immed), pos, end_pos));
   830       | SOME (text, (pos, end_pos)) =>
       
   831           (Method.finish_text (SOME text, immed), Position.set_range (pos, end_pos), end_pos));
   831   in
   832   in
   832     Seq.APPEND (fn state =>
   833     Seq.APPEND (fn state =>
   833       state
   834       state
   834       |> assert_forward
   835       |> assert_forward
   835       |> assert_bottom bot
   836       |> assert_bottom bot