diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/Infinite_Set.thy
--- a/src/HOL/Infinite_Set.thy	Thu Jul 07 12:36:56 2005 +0200
+++ b/src/HOL/Infinite_Set.thy	Thu Jul 07 12:39:17 2005 +0200
@@ -6,7 +6,7 @@
 header {* Infnite Sets and Related Concepts*}
 
 theory Infinite_Set
-imports Hilbert_Choice Finite_Set SetInterval
+imports Hilbert_Choice Binomial
 begin
 
 subsection "Infinite Sets"