refined Future.fork interfaces, no longer export Future.future;

--- a/src/Pure/Concurrent/par_list.ML	Thu Dec 04 23:46:20 2008 +0100
+++ b/src/Pure/Concurrent/par_list.ML	Thu Dec 04 23:46:20 2008 +0100
@@ -31,7 +31,7 @@
   if Future.enabled () then
     let
       val group = TaskQueue.new_group ();
-      val futures = map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs;
+      val futures = map (fn x => Future.fork_group group (fn () => f x)) xs;
       val _ = List.app (ignore o Future.join_result) futures;
     in Future.join_results futures end
   else map (Exn.capture f) xs;

--- a/src/Pure/Thy/thy_info.ML	Thu Dec 04 23:46:20 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML	Thu Dec 04 23:46:20 2008 +0100
@@ -323,8 +323,8 @@
     fun future (name, body) tab =
       let
         val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name);
-        val x = Future.future NONE deps true body;
-      in (x, Symtab.update (name, Future.task_of x) tab) end;
+        val x = Future.fork_deps deps body;
+      in (x, Symtab.update (name, x) tab) end;
     val _ = ignore (Exn.release_all (Future.join_results (#1 (fold_map future tasks Symtab.empty))));
   in () end;