# HG changeset patch
# User wenzelm
# Date 1120573009 -7200
# Node ID d3416641926f165a54e32de9e35adc9f3f28ba5c
# Parent  539b9cc282fa1ebc74738c8ee24b1f8da42edadf
List.app;
run both tests;

diff -r 539b9cc282fa -r d3416641926f 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;