--- a/src/Pure/Concurrent/unsynchronized.ML Sat Apr 09 20:07:10 2016 +0200
+++ b/src/Pure/Concurrent/unsynchronized.ML Sat Apr 09 20:14:00 2016 +0200
@@ -4,7 +4,19 @@
Raw ML references as unsynchronized state variables.
*)
-structure Unsynchronized =
+signature UNSYNCHRONIZED =
+sig
+ datatype ref = datatype ref
+ val := : 'a ref * 'a -> unit
+ val ! : 'a ref -> 'a
+ val change: 'a ref -> ('a -> 'a) -> unit
+ val change_result: 'a ref -> ('a -> 'b * 'a) -> 'b
+ val inc: int ref -> int
+ val dec: int ref -> int
+ val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
+end;
+
+structure Unsynchronized: UNSYNCHRONIZED =
struct
datatype ref = datatype ref;
@@ -29,5 +41,5 @@
end;
-val _ = ML_Name_Space.forget_val "ref";
-val _ = ML_Name_Space.forget_type "ref";
+ML_Name_Space.forget_val "ref";
+ML_Name_Space.forget_type "ref";