# HG changeset patch
# User wenzelm
# Date 1301675350 -7200
# Node ID d49ffc7a19f8368a79b3dedba868f2cf89fecd5c
# Parent  8df8e5cc31196c2345d61038be8b7a98d8e63474# Parent  ded5ba6b7bacfd6512f4e3077f56bd4cb3f69019
merged

diff -r 8df8e5cc3119 -r d49ffc7a19f8 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Fri Apr 01 17:20:56 2011 +0200
+++ b/src/Tools/quickcheck.ML	Fri Apr 01 18:29:10 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 *)