--- 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 =