--- a/src/Pure/Concurrent/multithreading.ML Fri Apr 08 22:48:25 2016 +0200
+++ b/src/Pure/Concurrent/multithreading.ML Sat Apr 09 11:21:38 2016 +0200
@@ -23,7 +23,6 @@
val tracing_time: bool -> Time.time -> (unit -> string) -> unit
val real_time: ('a -> unit) -> 'a -> Time.time
val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
- val serial: unit -> int
end;
structure Multithreading: MULTITHREADING =
@@ -147,24 +146,4 @@
val _ = Mutex.unlock lock;
in result end) ());
-
-(* serial numbers *)
-
-local
-
-val serial_lock = Mutex.mutex ();
-val serial_count = ref 0;
-
-in
-
-val serial = uninterruptible (fn _ => fn () =>
- let
- val _ = Mutex.lock serial_lock;
- val _ = serial_count := ! serial_count + 1;
- val res = ! serial_count;
- val _ = Mutex.unlock serial_lock;
- in res end);
-
end;
-
-end;