--- 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;