use Unsynchronized.change convenience, which also emphasizes the raw access to these references (which happen to be local here);
--- a/src/Tools/quickcheck.ML Fri Apr 01 16:29:58 2011 +0200
+++ b/src/Tools/quickcheck.ML Fri Apr 01 17:16:08 2011 +0200
@@ -115,12 +115,14 @@
timings = #timings r, reports = cons (size, report) (#reports r)}
| cons_report _ NONE result = result
-fun add_timing timing result_ref = (result_ref := cons_timing timing (!result_ref))
+fun add_timing timing result_ref =
+ Unsynchronized.change result_ref (cons_timing timing)
-fun add_report size report result_ref = (result_ref := cons_report size report (!result_ref))
+fun add_report size report result_ref =
+ Unsynchronized.change result_ref (cons_report size report)
fun add_response names eval_terms response result_ref =
- (result_ref := set_reponse names eval_terms response (!result_ref))
+ Unsynchronized.change result_ref (set_reponse names eval_terms response)
(* expectation *)