src/Pure/goal.ML
changeset 41776 3bd83302a3c3
parent 41703 d27950860514
child 41819 2d84831dc1a0
equal deleted inserted replaced
41775:6214816d79d3 41776:3bd83302a3c3
   113 fun forked i =
   113 fun forked i =
   114   Synchronized.change forked_proofs (fn m =>
   114   Synchronized.change forked_proofs (fn m =>
   115     let
   115     let
   116       val n = m + i;
   116       val n = m + i;
   117       val _ =
   117       val _ =
   118         Multithreading.tracing 1 (fn () =>
   118         Multithreading.tracing 2 (fn () =>
   119           ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
   119           ("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
   120     in n end);
   120     in n end);
   121 
   121 
   122 fun fork_name name e =
   122 fun fork_name name e =
   123   uninterruptible (fn _ => fn () =>
   123   uninterruptible (fn _ => fn () =>