src/Pure/goal.ML

   val protect: thm -> thm
   val conclude: thm -> thm
   val check_finished: Proof.context -> thm -> thm
   val finish: Proof.context -> thm -> thm
   val norm_result: thm -> thm
-  val fork_name: string -> (unit -> 'a) -> 'a future
-  val fork: (unit -> 'a) -> 'a future
+  val fork_name: string -> int -> (unit -> 'a) -> 'a future
+  val fork: int -> (unit -> 'a) -> 'a future
   val peek_futures: serial -> unit future list
   val reset_futures: unit -> Future.group list
   val future_enabled_level: int -> bool
   val future_enabled: unit -> bool
   val future_enabled_nested: int -> bool

   let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]
   in Output.status (implode (map (Markup.markup_only o props) markups)) end;
 
 in
 
-fun fork_name name e =
+fun fork_name name pri e =
   uninterruptible (fn _ => fn () =>
     let
       val pos = Position.thread_data ();
       val id = the_default 0 (Position.parse_id pos);
       val _ = count_forked 1;
 
       val future =
         (singleton o Future.forks)
-          {name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
+          {name = name, group = NONE, deps = [], pri = pri, interrupts = false}
           (fn () =>
             let
               val task = the (Future.worker_task ());
               val _ = status task [Markup.running];
               val result =

             in Exn.release result end);
       val _ = status (Future.task_of future) [Markup.forked];
       val _ = register_forked id future;
     in future end) ();
 
-fun fork e = fork_name "Goal.fork" e;
+fun fork pri e = fork_name "Goal.fork" pri e;
 
 fun forked_count () = #1 (Synchronized.value forked_proofs);
 
 fun peek_futures id =
   Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;

             else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
           end);
     val res =
       if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
       then result ()
-      else future_result ctxt' (fork result) (Thm.term_of stmt);
+      else future_result ctxt' (fork ~1 result) (Thm.term_of stmt);
   in
     Conjunction.elim_balanced (length props) res
     |> map (Assumption.export false ctxt' ctxt)
     |> Variable.export ctxt' ctxt
     |> map Drule.zero_var_indexes