reintroduce missing "critical"s by hand
authorblanchet
Thu, 16 Sep 2010 07:52:47 +0200
changeset 39445 c44e288f262b
parent 39444 beabb8443ee4
child 39446 7ed24d2dc7de
reintroduce missing "critical"s by hand
src/Tools/Metis/src/Normalize.sml
src/Tools/Metis/src/Useful.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 =
--- 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 =