--- a/src/Tools/misc_legacy.ML Fri Mar 14 15:41:29 2014 +0100
+++ b/src/Tools/misc_legacy.ML Fri Mar 14 16:54:01 2014 +0100
@@ -246,10 +246,11 @@
val char_vec = Vector.tabulate (62, gensym_char);
fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
-val gensym_seed = Unsynchronized.ref (0: int);
+val gensym_seed = Synchronized.var "gensym_seed" (0: int);
in
- fun gensym pre = pre ^ newid (CRITICAL (fn () => Unsynchronized.inc gensym_seed));
+ fun gensym pre =
+ Synchronized.change_result gensym_seed (fn i => (pre ^ newid i, i + 1));
end;