--- a/src/HOL/ex/ROOT.ML Fri Nov 29 15:07:27 1996 +0100
+++ b/src/HOL/ex/ROOT.ML Fri Nov 29 15:08:06 1996 +0100
@@ -21,7 +21,6 @@
time_use_thy "InSort";
time_use_thy "Qsort";
time_use_thy "LexProd";
-time_use_thy "Lagrange";
time_use_thy "Puzzle";
time_use_thy "Mutil";
time_use_thy "Primes";