diff -r 0b7337826593 -r 3fd79fcdb491 src/Pure/Concurrent/single_assignment_sequential.ML --- a/src/Pure/Concurrent/single_assignment_sequential.ML Thu Feb 18 17:07:10 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,30 +0,0 @@ -(* Title: Pure/Concurrent/single_assignment_sequential.ML - Author: Makarius - -Single-assignment variables (sequential version). -*) - -structure Single_Assignment: SINGLE_ASSIGNMENT = -struct - -abstype 'a var = Var of 'a SingleAssignment.saref -with - -fun var _ = Var (SingleAssignment.saref ()); - -fun peek (Var var) = SingleAssignment.savalue var; - -fun await v = - (case peek v of - SOME x => x - | NONE => Thread.unavailable ()); - -fun assign (v as Var var) x = - (case peek v of - SOME _ => raise Fail "Duplicate assignment to variable" - | NONE => SingleAssignment.saset (var, x)); - -end; - -end; -