renamed to multithreading_dummy.ML;
authorwenzelm
Tue, 24 Jul 2007 19:46:44 +0200
changeset 23968 091abf849a26
parent 23967 92130b24e87f
child 23969 ef782bbf2d09
renamed to multithreading_dummy.ML;
src/Pure/ML-Systems/no_multithreading.ML
--- a/src/Pure/ML-Systems/no_multithreading.ML	Tue Jul 24 19:44:39 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(*  Title:      Pure/ML-Systems/no_multithreading.ML
-    ID:         $Id$
-    Author:     Makarius
-
-Compatibility file for ML systems without multithreading.
-*)
-
-(*default number of worker threads*)
-val multithreading = ref (NONE: int option);
-
-(*critical section*)
-fun self_critical () = false;
-fun CRITICAL e = e ();