# HG changeset patch
# User wenzelm
# Date 1460225640 -7200
# Node ID 3c7a35c12e03048520af8d23bcef10e3afdbc2c7
# Parent  6e3fb0aa857a11177a73f812382ccf05d4d17998
proper signature for structure;
tuned;

diff -r 6e3fb0aa857a -r 3c7a35c12e03 src/Pure/Concurrent/unsynchronized.ML
--- 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";