--- a/src/HOL/Real/HahnBanach/Bounds.thy Wed Dec 10 22:46:42 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Wed Dec 10 23:13:21 2008 +0100
@@ -6,7 +6,7 @@
header {* Bounds *}
theory Bounds
-imports Main Real
+imports Main ContNotDenum
begin
locale lub =