# HG changeset patch
# User wenzelm
# Date 1185221883 -7200
# Node ID 4fbb1ff123376a2bbd972a5be13d48eabcc60333
# Parent  622641164de8b9f6639f576b88e021af74b07b72
added multithreading, self_critical

diff -r 622641164de8 -r 4fbb1ff12337 src/Pure/ML-Systems/no_multithreading.ML
--- a/src/Pure/ML-Systems/no_multithreading.ML	Mon Jul 23 22:18:01 2007 +0200
+++ b/src/Pure/ML-Systems/no_multithreading.ML	Mon Jul 23 22:18:03 2007 +0200
@@ -5,6 +5,9 @@
 Compatibility file for ML systems without multithreading.
 *)
 
-(* critical section *)
+(*default number of worker threads*)
+val multithreading = ref (NONE: int option);
 
+(*critical section*)
+fun self_critical () = false;
 fun CRITICAL e = e ();