--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML Wed Jul 21 16:29:20 2010 +0200
+++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML Wed Jul 21 16:49:52 2010 +0200
@@ -8,8 +8,8 @@
Unsynchronized.set timing;
warning "\nset quick_and_dirty\n"; Unsynchronized.set quick_and_dirty;
-List.app time_use_thy tests;
+use_thys tests;
warning "\nreset quick_and_dirty\n"; Unsynchronized.reset quick_and_dirty;
-List.app ThyInfo.remove_thy tests;
-List.app time_use_thy tests;
+List.app Thy_Info.remove_thy tests;
+use_thys tests;