reintroduce the CRITICAL sections from change 3880d21d6013

--- a/src/Tools/Metis/src/Clause.sml	Wed Sep 15 14:24:29 2010 +0200
+++ b/src/Tools/Metis/src/Clause.sml	Wed Sep 15 15:15:49 2010 +0200
@@ -16,7 +16,9 @@
     let
       val r = ref 0
     in
-      fn () => case r of ref n => let val () = r := n + 1 in n end
+      (* MODIFIED by Jasmin Blanchette *)
+      fn () => CRITICAL (fn () =>
+        case r of ref n => let val () = r := n + 1 in n end)
     end;
 
 (* ------------------------------------------------------------------------- *)

--- a/src/Tools/Metis/src/Normalize.sml	Wed Sep 15 14:24:29 2010 +0200
+++ b/src/Tools/Metis/src/Normalize.sml	Wed Sep 15 15:15:49 2010 +0200
@@ -689,7 +689,8 @@
     let
       val counter : int StringMap.map ref = ref (StringMap.new ())
     in
-      fn n =>
+      (* MODIFIED by Jasmin Blanchette *)
+      fn n => CRITICAL (fn () =>
          let
            val ref m = counter
            val s = Name.toString n
@@ -699,7 +700,7 @@
            val s = skolemPrefix ^ "_" ^ s ^ i
          in
            Name.fromString s
-         end
+         end)
     end;
 
 fun skolemize fv bv fm =
@@ -1243,13 +1244,14 @@
     let
       val counter : int ref = ref 0
     in
-      fn () =>
+      (* MODIFIED by Jasmin Blanchette *)
+      fn () => CRITICAL (fn () =>
          let
            val ref i = counter
            val () = counter := i + 1
          in
            definitionPrefix ^ "_" ^ Int.toString i
-         end
+         end)
     end;
 
 fun newDefinition def =

--- a/src/Tools/Metis/src/PortablePolyml.sml	Wed Sep 15 14:24:29 2010 +0200
+++ b/src/Tools/Metis/src/PortablePolyml.sml	Wed Sep 15 15:15:49 2010 +0200
@@ -56,6 +56,7 @@
       y
     end;
 
+
 (* ------------------------------------------------------------------------- *)
 (* Generating random values.                                                 *)
 (* ------------------------------------------------------------------------- *)

--- a/src/Tools/Metis/src/Random.sig	Wed Sep 15 14:24:29 2010 +0200
+++ b/src/Tools/Metis/src/Random.sig	Wed Sep 15 15:15:49 2010 +0200
@@ -8,6 +8,7 @@
 
 signature Random =
 sig
+  val CRITICAL: (unit -> 'a) -> 'a (* MODIFIED by Jasmin Blanchette *)
 
   val nextWord : unit -> word
 

--- a/src/Tools/Metis/src/Random.sml	Wed Sep 15 14:24:29 2010 +0200
+++ b/src/Tools/Metis/src/Random.sml	Wed Sep 15 15:15:49 2010 +0200
@@ -9,6 +9,9 @@
 structure Random :> Random =
 struct
 
+(* MODIFIED by Jasmin Blanchette *)
+fun CRITICAL e = NAMED_CRITICAL "metis" e;
+
 (* random words: 0w0 <= result <= max_word *)
 
 (*minimum length of unboxed words on all supported ML platforms*)
@@ -25,7 +28,8 @@
 
 fun change r f = r := f (!r);
 local val rand = (*Unsynchronized.*)ref 0w1
-in fun nextWord () = ((*Unsynchronized.*)change rand step; ! rand) end;
+(* MODIFIED by Jasmin Blanchette *)
+in fun nextWord () = CRITICAL (fn () => ((*Unsynchronized.*)change rand step; ! rand)) end;
 
 (*NB: higher bits are more random than lower ones*)
 fun nextBool () = Word.andb (nextWord (), top_bit) = 0w0;

--- a/src/Tools/Metis/src/Useful.sml	Wed Sep 15 14:24:29 2010 +0200
+++ b/src/Tools/Metis/src/Useful.sml	Wed Sep 15 15:15:49 2010 +0200
@@ -454,7 +454,8 @@
 
   val primesList = ref [2];
 in
-  fun primes n =
+  (* MODIFIED by Jasmin Blanchette *)
+  fun primes n = CRITICAL (fn () =>
       let
         val ref ps = primesList
 
@@ -469,10 +470,11 @@
           in
             ps
           end
-      end;
+      end);
 end;
 
-fun primesUpTo n =
+(* MODIFIED by Jasmin Blanchette *)
+fun primesUpTo n = CRITICAL (fn () =>
     let
       fun f k =
           let
@@ -484,7 +486,7 @@
           end
     in
       f 8
-    end;
+    end);
 
 (* ------------------------------------------------------------------------- *)
 (* Strings.                                                                  *)
@@ -702,22 +704,24 @@
 local
   val generator = ref 0
 in
-  fun newInt () =
+  (* MODIFIED by Jasmin Blanchette *)
+  fun newInt () = CRITICAL (fn () =>
       let
         val n = !generator
         val () = generator := n + 1
       in
         n
-      end;
+      end);
 
   fun newInts 0 = []
-    | newInts k =
+      (* MODIFIED by Jasmin Blanchette *)
+    | newInts k = CRITICAL (fn () =>
       let
         val n = !generator
         val () = generator := n + k
       in
         interval n k
-      end;
+      end);
 end;
 
 fun withRef (r,new) f x =