diff -r 67bfcd3a433c -r 1b99ee57d131 src/HOL/Real/HahnBanach/ROOT.ML
--- a/src/HOL/Real/HahnBanach/ROOT.ML	Fri Oct 29 19:24:20 1999 +0200
+++ b/src/HOL/Real/HahnBanach/ROOT.ML	Fri Oct 29 20:18:34 1999 +0200
@@ -5,5 +5,4 @@
 The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
 *)
 
-time_use_thy "Bounds";
 time_use_thy "HahnBanach";