# HG changeset patch
# User haftmann
# Date 1254736058 -7200
# Node ID e23a35f5400de3170dae2f7f09af8c390c8c9a07
# Parent  159309603edcf6ceda21813a50eb61b828f8d3b8
explicitly unsynchronized

diff -r 159309603edc -r e23a35f5400d Admin/Benchmarks/HOL-datatype/ROOT.ML
--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML	Sun Oct 04 12:59:22 2009 +0200
+++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML	Mon Oct 05 11:47:38 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      Admin/Benchmarks/HOL-datatype/ROOT.ML
-    ID:         $Id$
 
 Some rather large datatype examples (from John Harrison).
 *)
@@ -8,9 +7,9 @@
 
 set timing;
 
-warning "\nset quick_and_dirty\n"; set quick_and_dirty;
+warning "\nset quick_and_dirty\n"; Unsynchronized.set quick_and_dirty;
 List.app time_use_thy tests;
 
-warning "\nreset quick_and_dirty\n"; reset quick_and_dirty;
+warning "\nreset quick_and_dirty\n"; Unsynchronized.reset quick_and_dirty;
 List.app ThyInfo.remove_thy tests;
 List.app time_use_thy tests;