src/Pure/Concurrent/unsynchronized.ML
changeset 62818 2733b240bfea
parent 62508 d0b68218ea55
child 62891 7a11ea5c9626
--- a/src/Pure/Concurrent/unsynchronized.ML	Sat Apr 02 20:23:51 2016 +0200
+++ b/src/Pure/Concurrent/unsynchronized.ML	Sat Apr 02 20:33:34 2016 +0200
@@ -28,3 +28,6 @@
     in Exn.release result end) ();
 
 end;
+
+val _ = ML_Name_Space.forget_val "ref";
+val _ = ML_Name_Space.forget_type "ref";