Admin/Benchmarks/HOL-datatype/ROOT.ML

--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML	Tue Jul 05 15:49:19 2005 +0200
+++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML	Tue Jul 05 16:16:49 2005 +0200
@@ -9,10 +9,8 @@
 set timing;
 
 warning "\nset quick_and_dirty\n"; set quick_and_dirty;
-seq time_use_thy tests;
+List.app time_use_thy tests;
 
-(* not run by default
 warning "\nreset quick_and_dirty\n"; reset quick_and_dirty;
-seq remove_thy tests;
-seq time_use_thy tests;
-*)
+List.app remove_thy tests;
+List.app time_use_thy tests;