# HG changeset patch
# User wenzelm
# Date 1362333046 -3600
# Node ID a75040aaf369b60e44a601740bf62ae1629abf00
# Parent  bcd6b1aa4db5a83df045968c8ec01fcd078178f0
prefer more systematic Future.flat;

diff -r bcd6b1aa4db5 -r a75040aaf369 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sun Mar 03 17:34:42 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Sun Mar 03 18:50:46 2013 +0100
@@ -259,13 +259,13 @@
     val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
 
     val present =
-      singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE,
-        deps = map Future.task_of results, pri = 0, interrupts = true})
-      (fn () =>
-        let val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax () in
+      Future.flat results |> Future.map (fn res0 =>
+        let
+          val res = filter_out (Toplevel.is_ignored o #1) res0;
+          val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax ();
+        in
           Thy_Output.present_thy minor Keyword.command_tags
-            (Outer_Syntax.is_markup outer_syntax)
-            (filter_out (Toplevel.is_ignored o #1) (maps Future.join results)) toks
+            (Outer_Syntax.is_markup outer_syntax) res toks
           |> Buffer.content
           |> Present.theory_output name
         end);