diff -r 79e911c0c7d1 -r 776d888472aa Admin/Benchmarks/HOL-datatype/ROOT.ML
--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML	Fri Aug 27 10:49:12 1999 +0200
+++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML	Fri Aug 27 10:54:31 1999 +0200
@@ -1,10 +1,16 @@
-(*  Title:      Admin/Benchmarks/HOL-datatype/Brackin.thy
+(*  Title:      Admin/Benchmarks/HOL-datatype/ROOT.ML
     ID:         $Id$
 
 Some rather large datatype examples (from John Harrison).
 *)
 
-time_use_thy "Brackin";
-time_use_thy "Instructions";
-time_use_thy "SML";
-time_use_thy "Verilog";
+val tests = ["Brackin", "Instructions", "SML", "Verilog"];
+
+set Toplevel.trace;
+
+warning "\nset quick_and_dirty\n"; set quick_and_dirty;
+seq time_use_thy tests;
+
+warning "\nreset quick_and_dirty\n"; reset quick_and_dirty;
+seq remove_thy tests;
+seq time_use_thy tests;