# HG changeset patch
# User wenzelm
# Date 1254303942 -7200
# Node ID 8ae3a48c69d9f8295e2be04c11fd1fbf05a6d2d5
# Parent  1504f9c2d0605855809c93e51a30db1ea78cecfa
tuned whitespace;

diff -r 1504f9c2d060 -r 8ae3a48c69d9 src/Pure/ML-Systems/multithreading.ML
--- a/src/Pure/ML-Systems/multithreading.ML	Wed Sep 30 11:36:12 2009 +0200
+++ b/src/Pure/ML-Systems/multithreading.ML	Wed Sep 30 11:45:42 2009 +0200
@@ -24,7 +24,7 @@
   val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
   val sync_wait: Thread.threadAttribute list option -> Time.time option ->
     ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
-  val trace: int  Unsynchronized.ref
+  val trace: int Unsynchronized.ref
   val tracing: int -> (unit -> string) -> unit
   val tracing_time: bool -> Time.time -> (unit -> string) -> unit
   val real_time: ('a -> unit) -> 'a -> Time.time
@@ -38,7 +38,7 @@
 (* options *)
 
 val available = false;
-val max_threads =  Unsynchronized.ref (1: int);
+val max_threads = Unsynchronized.ref (1: int);
 fun max_threads_value () = 1: int;
 fun enabled () = false;
 
@@ -57,7 +57,7 @@
 
 (* tracing *)
 
-val trace =  Unsynchronized.ref (0: int);
+val trace = Unsynchronized.ref (0: int);
 fun tracing _ _ = ();
 fun tracing_time _ _ _ = ();
 fun real_time f x = (f x; Time.zeroTime);
@@ -72,7 +72,7 @@
 
 (* serial numbers *)
 
-local val count =  Unsynchronized.ref (0: int)
+local val count = Unsynchronized.ref (0: int)
 in fun serial () = (count := ! count + 1; ! count) end;
 
 end;