# HG changeset patch
# User blanchet
# Date 1284616367 -7200
# Node ID c44e288f262be2e6d41c5b148606d6c1c84bd664
# Parent  beabb8443ee4327d68f8c8e6323fdd10108482a4
reintroduce missing "critical"s by hand

diff -r beabb8443ee4 -r c44e288f262b src/Tools/Metis/src/Normalize.sml
--- a/src/Tools/Metis/src/Normalize.sml	Thu Sep 16 07:30:15 2010 +0200
+++ b/src/Tools/Metis/src/Normalize.sml	Thu Sep 16 07:52:47 2010 +0200
@@ -1245,13 +1245,13 @@
     let
       val counter : int ref = ref 0
     in
-      fn () =>
+      fn () => Portable.critical (fn () =>
          let
            val ref i = counter
            val () = counter := i + 1
          in
            definitionPrefix ^ "_" ^ Int.toString i
-         end
+         end) ()
     end;
 
 fun newDefinition def =
diff -r beabb8443ee4 -r c44e288f262b src/Tools/Metis/src/Useful.sml
--- a/src/Tools/Metis/src/Useful.sml	Thu Sep 16 07:30:15 2010 +0200
+++ b/src/Tools/Metis/src/Useful.sml	Thu Sep 16 07:52:47 2010 +0200
@@ -474,7 +474,7 @@
 
   val primesList = ref [2];
 in
-  fun primes n =
+  fun primes n = Portable.critical (fn () =>
       let
         val ref ps = primesList
 
@@ -489,10 +489,10 @@
           in
             ps
           end
-      end;
+      end) ();
 end;
 
-fun primesUpTo n =
+fun primesUpTo n = Portable.critical (fn () =>
     let
       fun f k =
           let
@@ -504,7 +504,7 @@
           end
     in
       f 8
-    end;
+    end) ();
 
 (* ------------------------------------------------------------------------- *)
 (* Strings.                                                                  *)
@@ -724,22 +724,22 @@
 local
   val generator = ref 0
 in
-  fun newInt () =
+  fun newInt () = Portable.critical (fn () =>
       let
         val n = !generator
         val () = generator := n + 1
       in
         n
-      end;
+      end) ();
 
   fun newInts 0 = []
-    | newInts k =
+    | newInts k = Portable.critical (fn () =>
       let
         val n = !generator
         val () = generator := n + k
       in
         interval n k
-      end;
+      end) ();
 end;
 
 fun withRef (r,new) f x =