src/Pure/Isar/toplevel.ML
changeset 51318 e6524a89c9e3
parent 51285 0859bd338c9b
child 51321 75682dfff630
     1.1 --- a/src/Pure/Isar/toplevel.ML	Thu Feb 28 18:35:31 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Feb 28 21:11:07 2013 +0100
     1.3 @@ -746,7 +746,7 @@
     1.4          val (body_trs, end_tr) = split_last proof_trs;
     1.5          val finish = Context.Theory o Proof_Context.theory_of;
     1.6  
     1.7 -        val future_proof = Proof.global_future_proof
     1.8 +        val future_proof = Proof.future_proof
     1.9            (fn prf =>
    1.10              setmp_thread_position head_tr (fn () =>
    1.11                Goal.fork_name "Toplevel.future_proof" (priority proof_trs)
    1.12 @@ -756,7 +756,7 @@
    1.13                        => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    1.14                      |> fold_map atom_result body_trs ||> command end_tr;
    1.15                    in (result, presentation_context_of result_state) end)) ())
    1.16 -          #-> Result.put;
    1.17 +          #> (fn (result, state') => state' |> Proof.global_done_proof |> Result.put result);
    1.18  
    1.19          val st'' = st'
    1.20            |> command (head_tr |> set_print false |> reset_trans |> end_proof (K future_proof));