added compatibility file for ML systems without multithreading;

--- a/src/Pure/IsaMakefile	Mon Jul 23 13:50:31 2007 +0200
+++ b/src/Pure/IsaMakefile	Mon Jul 23 14:06:11 2007 +0200
@@ -40,7 +40,8 @@
   Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML		\
   Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML	\
   Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML			\
-  ML-Systems/alice.ML ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML	\
+  ML-Systems/alice.ML ML-Systems/no_multithreading.ML 				\
+  ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML				\
   ML-Systems/polyml-5.0.ML ML-Systems/polyml-interrupt-timeout.ML		\
   ML-Systems/polyml-old-basis.ML ML-Systems/polyml-posix.ML 			\
   ML-Systems/polyml.ML ML-Systems/poplogml.ML ML-Systems/smlnj.ML		\

--- a/src/Pure/ML-Systems/alice.ML	Mon Jul 23 13:50:31 2007 +0200
+++ b/src/Pure/ML-Systems/alice.ML	Mon Jul 23 14:06:11 2007 +0200
@@ -13,6 +13,9 @@
 - Session.finish ();
 *)
 
+use "ML-Systems/no_multithreading.ML";
+
+
 fun exit 0 = (OS.Process.exit OS.Process.success): unit
   | exit _ = OS.Process.exit OS.Process.failure;
 

--- a/src/Pure/ML-Systems/mosml.ML	Mon Jul 23 13:50:31 2007 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Mon Jul 23 14:06:11 2007 +0200
@@ -29,6 +29,9 @@
 load "FileSys";
 load "IO";
 
+use "ML-Systems/no_multithreading.ML";
+
+
 (*low-level pointer equality*)
 local val cast : 'a -> int = Obj.magic
 in fun pointer_eq (x:'a, y:'a) = (cast x = cast y) end;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/no_multithreading.ML	Mon Jul 23 14:06:11 2007 +0200
@@ -0,0 +1,10 @@
+(*  Title:      Pure/ML-Systems/no_multithreading.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Compatibility file for ML systems without multithreading.
+*)
+
+(* critical section *)
+
+fun CRITICAL e = e ();

--- a/src/Pure/ML-Systems/polyml.ML	Mon Jul 23 13:50:31 2007 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Jul 23 14:06:11 2007 +0200
@@ -4,6 +4,9 @@
 Compatibility file for Poly/ML (version 4.1.x and 4.2.0).
 *)
 
+use "ML-Systems/no_multithreading.ML";
+
+
 (** ML system and platform related **)
 
 (* String compatibility *)

--- a/src/Pure/ML-Systems/smlnj.ML	Mon Jul 23 13:50:31 2007 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Mon Jul 23 14:06:11 2007 +0200
@@ -4,6 +4,8 @@
 Compatibility file for Standard ML of New Jersey 110 or later.
 *)
 
+use "ML-Systems/no_multithreading.ML";
+
 
 (** ML system related **)
 

--- a/src/Pure/Thy/thm_database.ML	Mon Jul 23 13:50:31 2007 +0200
+++ b/src/Pure/Thy/thm_database.ML	Mon Jul 23 14:06:11 2007 +0200
@@ -51,14 +51,15 @@
 fun ml_store_thm (name, thm) =
   let val thm' = store_thm (name, thm) in
     if warn_ml name then ()
-    else (qed_thms := [thm'];
-      use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);"))
+    else CRITICAL (fn () => (qed_thms := [thm'];
+      use_text_verbose ("val " ^ name ^ " = hd (! ThmDatabase.qed_thms);")))
   end;
 
 fun ml_store_thms (name, thms) =
   let val thms' = store_thms (name, thms) in
     if warn_ml name then ()
-    else (qed_thms := thms'; use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;"))
+    else CRITICAL (fn () => (qed_thms := thms';
+      use_text_verbose ("val " ^ name ^ " = ! ThmDatabase.qed_thms;")))
   end;