author | wenzelm |
Fri, 19 Dec 2014 23:27:00 +0100 | |
changeset 59160 | faaedc8222c8 |
parent 59159 | 9312710451f5 |
child 59161 | 5a13df748fac |
--- 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 =