src/Pure/goal.ML
changeset 37706 b16231572c61
parent 37186 349e9223c685
child 38474 1408f753bd75
     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