Admin/Benchmarks/HOL-datatype/ROOT.ML
changeset 9000 c20d58286a51
parent 7373 776d888472aa
child 10100 567b9676cb0a
--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -6,7 +6,7 @@
 
 val tests = ["Brackin", "Instructions", "SML", "Verilog"];
 
-set Toplevel.trace;
+set timing;
 
 warning "\nset quick_and_dirty\n"; set quick_and_dirty;
 seq time_use_thy tests;