diff -r a8b9191609a8 -r 7887eabb1997 Admin/Benchmarks/HOL-datatype/ROOT.ML
--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML	Wed Dec 14 15:05:22 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*  Title:      Admin/Benchmarks/HOL-datatype/ROOT.ML
-
-Some rather large datatype examples (from John Harrison).
-*)
-
-val tests = ["Brackin", "Instructions", "SML", "Verilog"];
-
-Toplevel.timing := true;
-
-warning "\nset quick_and_dirty\n"; quick_and_dirty := true;
-use_thys tests;
-
-warning "\nreset quick_and_dirty\n"; quick_and_dirty := false;
-List.app Thy_Info.remove_thy tests;
-use_thys tests;