src/Pure/RAW/single_assignment.ML
changeset 62357 ab76bd43c14a
parent 62353 7f927120b5a2
parent 62356 e307a410f46c
child 62358 0b7337826593
child 62359 6709e51d5c11
--- a/src/Pure/RAW/single_assignment.ML	Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(*  Title:      Pure/RAW/single_assignment.ML
-    Author:     Makarius
-
-References with single assignment.  Unsynchronized!
-*)
-
-signature SINGLE_ASSIGNMENT =
-sig
-  type 'a saref
-  exception Locked
-  val saref: unit -> 'a saref
-  val savalue: 'a saref -> 'a option
-  val saset: 'a saref * 'a -> unit
-end;
-
-structure SingleAssignment: SINGLE_ASSIGNMENT =
-struct
-
-exception Locked;
-
-abstype 'a saref = SARef of 'a option ref
-with
-
-fun saref () = SARef (ref NONE);
-
-fun savalue (SARef r) = ! r;
-
-fun saset (SARef (r as ref NONE), x) = r := SOME x
-  | saset _ = raise Locked;
-
-end;
-
-end;