--- a/src/HOL/ex/ROOT.ML Tue May 20 11:44:02 1997 +0200
+++ b/src/HOL/ex/ROOT.ML Tue May 20 11:44:25 1997 +0200
@@ -18,7 +18,6 @@
time_use_thy "BT";
time_use_thy "InSort";
time_use_thy "Qsort";
-time_use_thy "LexProd";
time_use_thy "Puzzle";
time_use_thy "Primes";
time_use_thy "NatSum";