diff -r 406ae5ced4e9 -r a42653373043 src/HOL/ex/ROOT.ML
--- 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";