recovered benchmarks, which are not tested automatically;
authorwenzelm
Wed, 21 Jul 2010 16:49:52 +0200
changeset 37875 496d723516e6
parent 37874 954dc0c580bd
child 37898 eb89d0ac75fb
recovered benchmarks, which are not tested automatically;
Admin/Benchmarks/HOL-datatype/ROOT.ML
--- 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;