1.1 --- a/src/Pure/Isar/proof.ML	Sun Jul 19 19:24:04 2009 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Mon Jul 20 00:37:39 2009 +0200
     1.3 @@ -1002,6 +1002,7 @@
     1.4      val _ = assert_backward state;
     1.5      val (goal_ctxt, (_, goal)) = find_goal state;
     1.6      val {statement as (kind, propss, prop), messages, using, goal, before_qed, after_qed} = goal;
     1.7 +    val goal_txt = prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt);
     1.8  
     1.9      val _ = is_relevant state andalso error "Cannot fork relevant proof";
    1.10  
    1.11 @@ -1017,13 +1018,13 @@
    1.12  
    1.13      val result_ctxt =
    1.14        state
    1.15 -      |> map_contexts (Variable.declare_term prop)
    1.16 +      |> map_contexts (fold Variable.declare_term goal_txt)
    1.17        |> map_goal I (K (statement', messages, using, goal', before_qed, after_qed'))
    1.18        |> fork_proof;
    1.19  
    1.20      val future_thm = result_ctxt |> Future.map (fn (_, x) =>
    1.21        ProofContext.get_fact_single (get_context x) (Facts.named this_name));
    1.22 -    val finished_goal = exception_trace (fn () => Goal.future_result goal_ctxt future_thm prop');
    1.23 +    val finished_goal = Goal.future_result goal_ctxt future_thm prop';
    1.24      val state' =
    1.25        state
    1.26        |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
    1.27 @@ -1045,7 +1046,7 @@
    1.28  fun future_terminal_proof proof1 proof2 meths int state =
    1.29    if int orelse is_relevant state orelse not (Goal.local_future_enabled ())
    1.30    then proof1 meths state
    1.31 -  else snd (proof2 (fn state' => Future.fork_local ~1 (fn () => ((), proof1 meths state'))) state);
    1.32 +  else snd (proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))) state);
    1.33  
    1.34  in
    1.35  

     2.1 --- a/src/Pure/Isar/toplevel.ML	Sun Jul 19 19:24:04 2009 +0200
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Jul 20 00:37:39 2009 +0200
     2.3 @@ -652,7 +652,7 @@
     2.4  
     2.5          val future_proof = Proof.global_future_proof
     2.6            (fn prf =>
     2.7 -            Future.fork_local ~1 (fn () =>
     2.8 +            Future.fork_pri ~1 (fn () =>
     2.9                let val (states, result_state) =
    2.10                  (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
    2.11                    => State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))

     3.1 --- a/src/Pure/goal.ML	Sun Jul 19 19:24:04 2009 +0200
     3.2 +++ b/src/Pure/goal.ML	Mon Jul 20 00:37:39 2009 +0200
     3.3 @@ -188,7 +188,7 @@
     3.4      val res =
     3.5        if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
     3.6        then result ()
     3.7 -      else future_result ctxt' (Future.fork_local ~1 result) (Thm.term_of stmt);
     3.8 +      else future_result ctxt' (Future.fork_pri ~1 result) (Thm.term_of stmt);
     3.9    in
    3.10      Conjunction.elim_balanced (length props) res
    3.11      |> map (Assumption.export false ctxt' ctxt)