1.1 --- a/src/Pure/goal.ML Sun Jul 04 00:05:32 2010 +0200
1.2 +++ b/src/Pure/goal.ML Sun Jul 04 21:01:22 2010 +0200
1.3 @@ -104,12 +104,7 @@
1.4
1.5 (* parallel proofs *)
1.6
1.7 -fun fork e = Future.fork_pri ~1 (fn () =>
1.8 - let
1.9 - val _ = Output.status (Markup.markup Markup.forked "");
1.10 - val x = e (); (*sic*)
1.11 - val _ = Output.status (Markup.markup Markup.joined "");
1.12 - in x end);
1.13 +fun fork e = Future.fork_pri ~1 (fn () => Future.report e);
1.14
1.15 val parallel_proofs = Unsynchronized.ref 1;
1.16