src/Pure/library.ML

   val not_equal: ''a -> ''a -> bool
   val orf: ('a -> bool) * ('a -> bool) -> 'a -> bool
   val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool
   val exists: ('a -> bool) -> 'a list -> bool
   val forall: ('a -> bool) -> 'a list -> bool
-  val set: bool ref -> bool
-  val reset: bool ref -> bool
-  val toggle: bool ref -> bool
-  val change: 'a ref -> ('a -> 'a) -> unit
-  val change_result: 'a ref -> ('a -> 'b * 'a) -> 'b
-  val setmp_noncritical: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
-  val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
+  val setmp_noncritical: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
+  val setmp: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
   val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
 
   (*lists*)
   exception UnequalLengths
   val single: 'a -> 'a list

   val prefixes: 'a list -> 'a list list
   val suffixes1: 'a list -> 'a list list
   val suffixes: 'a list -> 'a list list
 
   (*integers*)
-  val inc: int ref -> int
-  val dec: int ref -> int
   val upto: int * int -> int list
   val downto: int * int -> int list
   val radixpand: int * int -> int list
   val radixstring: int * string * int -> string
   val string_of_int: int -> string

 val forall = List.all;
 
 
 (* flags *)
 
-fun set flag = (flag := true; true);
-fun reset flag = (flag := false; false);
-fun toggle flag = (flag := not (! flag); ! flag);
-
-fun change r f = r := f (! r);
-fun change_result r f = let val (x, y) = f (! r) in r := y; x end;
-
 (*temporarily set flag during execution*)
 fun setmp_noncritical flag value f x =
   uninterruptible (fn restore_attributes => fn () =>
     let
       val orig_value = ! flag;

 fun suffixes xs = [] :: suffixes1 xs;
 
 
 
 (** integers **)
-
-fun inc i = (i := ! i + (1: int); ! i);
-fun dec i = (i := ! i - (1: int); ! i);
-
 
 (* lists of integers *)
 
 (*make the list [from, from + 1, ..., to]*)
 fun ((i: int) upto j) =

 fun rmod x y = x - y * Real.realFloor (x / y);
 
 local
   val a = 16807.0;
   val m = 2147483647.0;
-  val random_seed = ref 1.0;
+  val random_seed = Unsynchronized.ref 1.0;
 in
 
 fun random () = CRITICAL (fn () =>
   let val r = rmod (a * ! random_seed) m
   in (random_seed := r; r) end);

   else chr (ord "0" + i - 52);
 
 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 = ref (0: int);
+val gensym_seed = Unsynchronized.ref (0: int);
 
 in
-  fun gensym pre = pre ^ newid (NAMED_CRITICAL "gensym" (fn () => inc gensym_seed));
+  fun gensym pre =
+    pre ^ newid (NAMED_CRITICAL "gensym" (fn () => Unsynchronized.inc gensym_seed));
 end;
 
 
 (* stamps and serial numbers *)
 
-type stamp = unit ref;
-val stamp: unit -> stamp = ref;
+type stamp = unit Unsynchronized.ref;
+val stamp: unit -> stamp = Unsynchronized.ref;
 
 type serial = int;
 val serial = Multithreading.serial;
 val serial_string = string_of_int o serial;