| changeset 59160 | faaedc8222c8 |
| parent 52537 | 4b5941730bd8 |
| child 59195 | f8588372d70e |
--- a/src/Pure/Concurrent/synchronized_sequential.ML Fri Dec 19 23:01:46 2014 +0100 +++ b/src/Pure/Concurrent/synchronized_sequential.ML Fri Dec 19 23:27:00 2014 +0100 @@ -11,6 +11,7 @@ with fun var _ x = Var (Unsynchronized.ref x); +fun peek (Var var) = ! var; fun value (Var var) = ! var; fun timed_access (Var var) _ f =