src/Pure/Isar/toplevel.ML
changeset 41673 1c191a39549f
parent 41536 47fef6afe756
child 41674 7da257539a8d
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Jan 31 21:54:49 2011 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Jan 31 22:57:01 2011 +0100
     1.3 @@ -663,13 +663,15 @@
     1.4  
     1.5          val future_proof = Proof.global_future_proof
     1.6            (fn prf =>
     1.7 -            Future.fork_pri ~1 (fn () =>
     1.8 -              let val (states, result_state) =
     1.9 -                (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
    1.10 -                  => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    1.11 -                |> fold_map command_result body_trs
    1.12 -                ||> command (end_tr |> set_print false);
    1.13 -              in (states, presentation_context_of result_state) end))
    1.14 +            singleton
    1.15 +              (Future.bulk {name = "Toplevel.proof_result", group = NONE, deps = [], pri = ~1})
    1.16 +              (fn () =>
    1.17 +                let val (states, result_state) =
    1.18 +                  (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
    1.19 +                    => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
    1.20 +                  |> fold_map command_result body_trs
    1.21 +                  ||> command (end_tr |> set_print false);
    1.22 +                in (states, presentation_context_of result_state) end))
    1.23            #> (fn (states, ctxt) => States.put (SOME states) ctxt);
    1.24  
    1.25          val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));