# HG changeset patch
# User wenzelm
# Date 1279723792 -7200
# Node ID 496d723516e627977cb9e81771f59dc415f7efb1
# Parent  954dc0c580bd8972bca8a3214e95804c677bb60d
recovered benchmarks, which are not tested automatically;

diff -r 954dc0c580bd -r 496d723516e6 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;