src/Pure/Concurrent/synchronized.ML
changeset 33689 d0a9ce721e0c
parent 33060 e66b41782cb5
child 35015 efafb3337ef3