# HG changeset patch
# User wenzelm
# Date 1248043059 -7200
# Node ID 457f5bcd3d76c5c85db5d40d0b06d592714e29a7
# Parent  11f8ee55662da5d2761cc65a988236f4bd737059
Proof.future_proof: declare all assumptions as well;
Proof.future_proof: removed spurious exception_trace (which might cause crash-by-interrupt);
replaced Future.fork_local by Future.fork_pri (again, until group exceptions are propagated properly);

diff -r 11f8ee55662d -r 457f5bcd3d76 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Jul 19 19:24:04 2009 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Jul 20 00:37:39 2009 +0200
@@ -1002,6 +1002,7 @@
     val _ = assert_backward state;
     val (goal_ctxt, (_, goal)) = find_goal state;
     val {statement as (kind, propss, prop), messages, using, goal, before_qed, after_qed} = goal;
+    val goal_txt = prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt);
 
     val _ = is_relevant state andalso error "Cannot fork relevant proof";
 
@@ -1017,13 +1018,13 @@
 
     val result_ctxt =
       state
-      |> map_contexts (Variable.declare_term prop)
+      |> map_contexts (fold Variable.declare_term goal_txt)
       |> map_goal I (K (statement', messages, using, goal', before_qed, after_qed'))
       |> fork_proof;
 
     val future_thm = result_ctxt |> Future.map (fn (_, x) =>
       ProofContext.get_fact_single (get_context x) (Facts.named this_name));
-    val finished_goal = exception_trace (fn () => Goal.future_result goal_ctxt future_thm prop');
+    val finished_goal = Goal.future_result goal_ctxt future_thm prop';
     val state' =
       state
       |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
@@ -1045,7 +1046,7 @@
 fun future_terminal_proof proof1 proof2 meths int state =
   if int orelse is_relevant state orelse not (Goal.local_future_enabled ())
   then proof1 meths state
-  else snd (proof2 (fn state' => Future.fork_local ~1 (fn () => ((), proof1 meths state'))) state);
+  else snd (proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))) state);
 
 in
 
diff -r 11f8ee55662d -r 457f5bcd3d76 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Jul 19 19:24:04 2009 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Jul 20 00:37:39 2009 +0200
@@ -652,7 +652,7 @@
 
         val future_proof = Proof.global_future_proof
           (fn prf =>
-            Future.fork_local ~1 (fn () =>
+            Future.fork_pri ~1 (fn () =>
               let val (states, result_state) =
                 (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
                   => State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
diff -r 11f8ee55662d -r 457f5bcd3d76 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sun Jul 19 19:24:04 2009 +0200
+++ b/src/Pure/goal.ML	Mon Jul 20 00:37:39 2009 +0200
@@ -188,7 +188,7 @@
     val res =
       if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
       then result ()
-      else future_result ctxt' (Future.fork_local ~1 result) (Thm.term_of stmt);
+      else future_result ctxt' (Future.fork_pri ~1 result) (Thm.term_of stmt);
   in
     Conjunction.elim_balanced (length props) res
     |> map (Assumption.export false ctxt' ctxt)